feat(data/polynomial/{ basic + div + monic + degree/definitions }): l…

…emmas about monic and forall_eq (#15817)

This PR reorganizes a couple of lemmas about monic.  The main breaking change is the removal of `subsingleton_of_monic_zero'` in favour of `monic_zero_iff_subsingleton`.

I left in `monic_zero_iff_subsingleton'` an iff version of `subsingleton_of_monic_zero'`, but I think that this can probably be removed, thanks to `monic_zero_iff_subsingleton` and `forall_eq_iff_forall_eq`.

Also, if anyone wants to rename some/all subsingletons to forall_eq, I am happy to do the change!

src/data/polynomial/basic.lean

@@ -480,6 +480,15 @@ lemma monomial_eq_C_mul_X : ∀{n}, monomial n a = C a * X^n
 calc C a = 0 ↔ C a = C 0 : by rw C_0
          ... ↔ a = 0 : C_inj
 
+lemma subsingleton_iff_subsingleton :
+  subsingleton R[X] ↔ subsingleton R :=
+⟨λ h, subsingleton_iff.mpr (λ a b, C_inj.mp (subsingleton_iff.mp h _ _)),
+  by { introI, apply_instance } ⟩
+
+lemma forall_eq_iff_forall_eq :
+  (∀ f g : R[X], f = g) ↔ (∀ a b : R, a = b) :=
+by simpa only [← subsingleton_iff] using subsingleton_iff_subsingleton
+
 theorem ext_iff {p q : R[X]} : p = q ↔ ∀ n, coeff p n = coeff q n :=
 by { rcases p, rcases q, simp [coeff, finsupp.ext_iff] }
 

src/data/polynomial/degree/definitions.lean

@@ -839,12 +839,6 @@ begin
       exact coeff_mul_degree_add_degree _ _ } }
 end
 
-lemma subsingleton_of_monic_zero (h : monic (0 : R[X])) :
-  (∀ p q : R[X], p = q) ∧ (∀ a b : R, a = b) :=
-by rw [monic.def, leading_coeff_zero] at h;
-  exact ⟨λ p q, by rw [← mul_one p, ← mul_one q, ← C_1, ← h, C_0, mul_zero, mul_zero],
-    λ a b, by rw [← mul_one a, ← mul_one b, ← h, mul_zero, mul_zero]⟩
-
 lemma zero_le_degree_iff {p : R[X]} : 0 ≤ degree p ↔ p ≠ 0 :=
 by rw [ne.def, ← degree_eq_bot];
   cases degree p; exact dec_trivial

src/data/polynomial/div.lean

@@ -150,12 +150,12 @@ begin
 end
 
 @[simp] lemma mod_by_monic_zero (p : R[X]) : p %ₘ 0 = p :=
-if h : monic (0 : R[X]) then (subsingleton_of_monic_zero h).1 _ _ else
-by unfold mod_by_monic div_mod_by_monic_aux; rw dif_neg h
+if h : monic (0 : R[X]) then by { haveI := monic_zero_iff_subsingleton.mp h, simp }
+else by unfold mod_by_monic div_mod_by_monic_aux; rw dif_neg h
 
 @[simp] lemma div_by_monic_zero (p : R[X]) : p /ₘ 0 = 0 :=
-if h : monic (0 : R[X]) then (subsingleton_of_monic_zero h).1 _ _ else
-by unfold div_by_monic div_mod_by_monic_aux; rw dif_neg h
+if h : monic (0 : R[X]) then by { haveI := monic_zero_iff_subsingleton.mp h, simp }
+else by unfold div_by_monic div_mod_by_monic_aux; rw dif_neg h
 
 lemma div_by_monic_eq_of_not_monic (p : R[X]) (hq : ¬monic q) : p /ₘ q = 0 := dif_neg hq
 

src/data/polynomial/monic.lean

@@ -26,6 +26,17 @@ variables {R : Type u} {S : Type v} {a b : R} {m n : ℕ} {ι : Type y}
 section semiring
 variables [semiring R] {p q r : R[X]}
 
+lemma monic_zero_iff_subsingleton : monic (0 : R[X]) ↔ subsingleton R :=
+subsingleton_iff_zero_eq_one
+
+lemma not_monic_zero_iff : ¬ monic (0 : R[X]) ↔ (0 : R) ≠ 1 :=
+(monic_zero_iff_subsingleton.trans subsingleton_iff_zero_eq_one.symm).not
+
+lemma monic_zero_iff_subsingleton' :
+  monic (0 : R[X]) ↔ (∀ f g : R[X], f = g) ∧ (∀ a b : R, a = b) :=
+polynomial.monic_zero_iff_subsingleton.trans ⟨by { introI, simp },
+  λ h, subsingleton_iff.mpr h.2⟩
+
 lemma monic.as_sum (hp : p.monic) :
   p = X^(p.nat_degree) + (∑ i in range p.nat_degree, C (p.coeff i) * X^i) :=
 begin
@@ -392,7 +403,7 @@ section nonzero_semiring
 variables [semiring R] [nontrivial R] {p q : R[X]}
 
 @[simp] lemma not_monic_zero : ¬monic (0 : R[X]) :=
-by simpa only [monic, leading_coeff_zero] using (zero_ne_one : (0 : R) ≠ 1)
+not_monic_zero_iff.mp zero_ne_one
 
 end nonzero_semiring