minimal_polynomial_degree_one

Stream: Is there code for X?

[Thomas Browning]

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]

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]

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