feat(data/polynomial/monic): monic.is_regular (#8679)

This golfs/generalizes some proofs.
Additionally, provide some helper API for `is_regular`,
for non-zeros in domains,
and for smul of units.



Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/algebra/regular/smul.lean

@@ -188,11 +188,25 @@ end comm_monoid
 
 end is_smul_regular
 
+section group
+
+variables {G : Type*} [group G]
+
+/-- An element of a group acting on a Type is regular. This relies on the availability
+of the inverse given by groups, since there is no `left_cancel_smul` typeclass. -/
+lemma is_smul_regular_of_group [mul_action G R] (g : G) : is_smul_regular R g :=
+begin
+  intros x y h,
+  convert congr_arg ((•) g⁻¹) h using 1;
+  simp [←smul_assoc]
+end
+
+end group
+
 variables [monoid_with_zero R] [has_zero M] [mul_action_with_zero R M]
 
 /-- Any element in `units R` is `M`-regular. -/
-lemma units.is_smul_regular (a : units R) : is_smul_regular M (a : R)
-:=
+lemma units.is_smul_regular (a : units R) : is_smul_regular M (a : R) :=
 is_smul_regular.of_mul_eq_one a.inv_val
 
 /-- A unit is `M`-regular. -/

src/algebra/ring/basic.lean

@@ -920,7 +920,7 @@ lemma is_regular_of_ne_zero' [ring α] [no_zero_divisors α] {k : α} (hk : k 
   is_regular k :=
 ⟨is_left_regular_of_non_zero_divisor k
   (λ x h, (no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left hk),
-  is_right_regular_of_non_zero_divisor k
+ is_right_regular_of_non_zero_divisor k
   (λ x h, (no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hk)⟩
 
 /-- A domain is a ring with no zero divisors, i.e. satisfying

src/data/polynomial/monic.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import data.polynomial.reverse
 import algebra.associated
+import algebra.regular.smul
 
 /-!
 # Theory of monic polynomials
@@ -332,7 +333,6 @@ end nonzero_semiring
 section not_zero_divisor
 
 -- TODO: using gh-8537, rephrase lemmas that involve commutation around `*` using the op-ring
--- TODO: using gh-8561, rephrase using regular elements
 
 variables [semiring R] {p : polynomial R}
 
@@ -385,8 +385,18 @@ begin
   simp [h.mul_left_ne_zero, hq]
 end
 
-lemma degree_smul_of_non_zero_divisor {S : Type*} [monoid S] [distrib_mul_action S R]
-  (p : polynomial R) (k : S) (h : ∀ (x : R), k • x = 0 → x = 0) :
+lemma monic.is_regular {R : Type*} [ring R] {p : polynomial R} (hp : monic p) : is_regular p :=
+begin
+  split,
+  { intros q r h,
+    rw [←sub_eq_zero, ←hp.mul_right_eq_zero_iff, mul_sub, h, sub_self] },
+  { intros q r h,
+    simp only at h,
+    rw [←sub_eq_zero, ←hp.mul_left_eq_zero_iff, sub_mul, h, sub_self] }
+end
+
+lemma degree_smul_of_smul_regular {S : Type*} [monoid S] [distrib_mul_action S R]
+  {k : S} (p : polynomial R) (h : is_smul_regular R k) :
   (k • p).degree = p.degree :=
 begin
   refine le_antisymm _ _,
@@ -397,38 +407,35 @@ begin
   { rw degree_le_iff_coeff_zero,
     intros m hm,
     rw degree_lt_iff_coeff_zero at hm,
-    refine h _ _,
+    refine h _,
     simpa using hm m le_rfl },
 end
 
-lemma nat_degree_smul_of_non_zero_divisor {S : Type*} [monoid S] [distrib_mul_action S R]
-  (p : polynomial R) (k : S) (h : ∀ (x : R), k • x = 0 → x = 0) :
+lemma nat_degree_smul_of_smul_regular {S : Type*} [monoid S] [distrib_mul_action S R]
+  {k : S} (p : polynomial R) (h : is_smul_regular R k) :
   (k • p).nat_degree = p.nat_degree :=
 begin
   by_cases hp : p = 0,
   { simp [hp] },
   rw [←with_bot.coe_eq_coe, ←degree_eq_nat_degree hp, ←degree_eq_nat_degree,
-      degree_smul_of_non_zero_divisor _ _ h],
+      degree_smul_of_smul_regular p h],
   contrapose! hp,
-  rw polynomial.ext_iff at hp ⊢,
-  simp only [coeff_smul, coeff_zero] at hp,
-  intro n,
-  simp [h _ (hp n)]
+  rw ←smul_zero k at hp,
+  exact h.polynomial hp
 end
 
-lemma leading_coeff_smul_of_non_zero_divisor {S : Type*} [monoid S] [distrib_mul_action S R]
-  (p : polynomial R) (k : S) (h : ∀ (x : R), k • x = 0 → x = 0) :
+lemma leading_coeff_smul_of_smul_regular {S : Type*} [monoid S] [distrib_mul_action S R]
+  {k : S} (p : polynomial R) (h : is_smul_regular R k) :
   (k • p).leading_coeff = k • p.leading_coeff :=
-by rw [leading_coeff, leading_coeff, coeff_smul, nat_degree_smul_of_non_zero_divisor _ _ h]
+by rw [leading_coeff, leading_coeff, coeff_smul, nat_degree_smul_of_smul_regular p h]
 
 lemma monic_of_is_unit_leading_coeff_inv_smul (h : is_unit p.leading_coeff) :
   monic (h.unit⁻¹ • p) :=
 begin
-  rw [monic.def, leading_coeff_smul_of_non_zero_divisor, units.smul_def],
-  { obtain ⟨k, hk⟩ := h,
-    simp only [←hk, smul_eq_mul, ←units.coe_mul, units.coe_eq_one, inv_mul_eq_iff_eq_mul],
-    simp [units.ext_iff, is_unit.unit_spec] },
-  { simp [smul_eq_zero_iff_eq] }
+  rw [monic.def, leading_coeff_smul_of_smul_regular _ (is_smul_regular_of_group _), units.smul_def],
+  obtain ⟨k, hk⟩ := h,
+  simp only [←hk, smul_eq_mul, ←units.coe_mul, units.coe_eq_one, inv_mul_eq_iff_eq_mul],
+  simp [units.ext_iff, is_unit.unit_spec]
 end
 
 lemma is_unit_leading_coeff_mul_right_eq_zero_iff (h : is_unit p.leading_coeff) {q : polynomial R} :
@@ -437,13 +444,13 @@ begin
   split,
   { intro hp,
     rw ←smul_eq_zero_iff_eq (h.unit)⁻¹ at hp,
-    { have : (h.unit)⁻¹ • (p * q) = ((h.unit)⁻¹ • p) * q,
-      { ext,
-        simp only [units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum],
-        refine sum_congr rfl (λ x hx, _),
-        rw ←mul_assoc },
-      rwa [this, monic.mul_right_eq_zero_iff] at hp,
-      exact monic_of_is_unit_leading_coeff_inv_smul _ } },
+    have : (h.unit)⁻¹ • (p * q) = ((h.unit)⁻¹ • p) * q,
+    { ext,
+      simp only [units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum],
+      refine sum_congr rfl (λ x hx, _),
+      rw ←mul_assoc },
+    rwa [this, monic.mul_right_eq_zero_iff] at hp,
+    exact monic_of_is_unit_leading_coeff_inv_smul _ },
   { rintro rfl,
     simp }
 end