feat(data/polynomial,field_theory): (minpoly A x).map f ≠ 1 (#9451)

We use this result to generalize `minpoly.not_is_unit` from integral domains to nontrivial `comm_ring`s.





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/polynomial/monic.lean

@@ -165,6 +165,20 @@ begin
     simp [coeff_mul, nat.antidiagonal, hp.leading_coeff, hq.leading_coeff, add_comm]
 end
 
+lemma eq_one_of_map_eq_one {S : Type*} [semiring S] [nontrivial S]
+  (f : R →+* S) (hp : p.monic) (map_eq : p.map f = 1) : p = 1 :=
+begin
+  nontriviality R,
+  have hdeg : p.degree = 0,
+  { rw [← degree_map_eq_of_leading_coeff_ne_zero f _, map_eq, degree_one],
+    { rw [hp.leading_coeff, f.map_one],
+      exact one_ne_zero } },
+  have hndeg : p.nat_degree = 0 :=
+    with_bot.coe_eq_coe.mp ((degree_eq_nat_degree hp.ne_zero).symm.trans hdeg),
+  convert eq_C_of_degree_eq_zero hdeg,
+  rw [← hndeg, ← polynomial.leading_coeff, hp.leading_coeff, C.map_one]
+end
+
 end monic
 
 end semiring

src/field_theory/minpoly.lean

@@ -69,6 +69,31 @@ begin
   { exact aeval_zero _ }
 end
 
+/-- A minimal polynomial is not `1`. -/
+lemma ne_one [nontrivial B] : minpoly A x ≠ 1 :=
+begin
+  intro h,
+  refine (one_ne_zero : (1 : B) ≠ 0) _,
+  simpa using congr_arg (polynomial.aeval x) h
+end
+
+lemma map_ne_one [nontrivial B] {R : Type*} [semiring R] [nontrivial R] (f : A →+* R) :
+  (minpoly A x).map f ≠ 1 :=
+begin
+  by_cases hx : is_integral A x,
+  { exact mt ((monic hx).eq_one_of_map_eq_one f) (ne_one A x) },
+  { rw [eq_zero hx, polynomial.map_zero], exact zero_ne_one },
+end
+
+/-- A minimal polynomial is not a unit. -/
+lemma not_is_unit [nontrivial B] : ¬ is_unit (minpoly A x) :=
+begin
+  haveI : nontrivial A := (algebra_map A B).domain_nontrivial,
+  by_cases hx : is_integral A x,
+  { exact mt (eq_one_of_is_unit_of_monic (monic hx)) (ne_one A x) },
+  { rw [eq_zero hx], exact not_is_unit_zero }
+end
+
 lemma mem_range_of_degree_eq_one (hx : (minpoly A x).degree = 1) : x ∈ (algebra_map A B).range :=
 begin
   have h : is_integral A x,
@@ -146,16 +171,6 @@ begin
   simp only [h0, ring_hom.map_neg, sub_eq_add_neg],
 end
 
-variables (A x)
-
-/-- A minimal polynomial is not a unit. -/
-lemma not_is_unit : ¬ is_unit (minpoly A x) :=
-begin
-  by_cases hx : is_integral A x,
-  { assume H, exact (ne_of_lt (degree_pos hx)).symm (degree_eq_zero_of_is_unit H) },
-  { delta minpoly, rw dif_neg hx, simp only [not_is_unit_zero, not_false_iff] }
-end
-
 end ring
 
 section domain