## Stream: Is there code for X?

### Topic: minimal_polynomial_degree_one

#### Thomas Browning (Jan 22 2021 at 00:49):

This result doesn't seem to be in mathlib, and would be a good lemma for minpoly.lean:

lemma my_lemma {A B : Type*} [comm_ring A] [ring B] [algebra A B] {b : B}
(hb : (minpoly A b).degree = 1) : b ∈ (algebra_map A B).range := sorry


There seem to be several ways to prove this, but I can't seem to find the necessary sublemmas in mathlib.

For instance, does mathlib know that a polynomial of degree 1 has a unique root?

#### Thomas Browning (Jan 22 2021 at 00:55):

It seems like you can prove that a polynomial of degree 1 has a unique root with overpowered machinery: (splits_of_degree_eq_one and degree_eq_card_roots in splitting_field.lean, but these results can't be used in minpoly.lean)

#### Thomas Browning (Jan 22 2021 at 02:57):

I've got a proof now. It's not the prettiest, but it'll be in an upcoming PR.

Last updated: May 07 2021 at 22:14 UTC