Zulip Chat Archive

Stream: Is there code for X?

Topic: minimal_polynomial_degree_one


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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