feat(ring_theory/multiplicity): generalize multiplicity (#16330)

Divisibility is defined for any `semigroup`, so I also reduce the assumption of `multiplicity` to any `monoid`. At least it can be used for the elements which commute with every element, such as `power_series.X`.

- [x] depends on: #16328

src/ring_theory/multiplicity.lean

@@ -29,13 +29,13 @@ open_locale big_operators
 /-- `multiplicity a b` returns the largest natural number `n` such that
   `a ^ n ∣ b`, as an `part_enat` or natural with infinity. If `∀ n, a ^ n ∣ b`,
   then it returns `⊤`-/
-def multiplicity [comm_monoid α] [decidable_rel ((∣) : α → α → Prop)] (a b : α) : part_enat :=
+def multiplicity [monoid α] [decidable_rel ((∣) : α → α → Prop)] (a b : α) : part_enat :=
 part_enat.find $ λ n, ¬a ^ (n + 1) ∣ b
 
 namespace multiplicity
 
-section comm_monoid
-variables [comm_monoid α]
+section monoid
+variables [monoid α]
 
 /-- `multiplicity.finite a b` indicates that the multiplicity of `a` in `b` is finite. -/
 @[reducible] def finite (a b : α) : Prop := ∃ n : ℕ, ¬a ^ (n + 1) ∣ b
@@ -45,6 +45,9 @@ lemma finite_iff_dom [decidable_rel ((∣) : α → α → Prop)] {a b : α} :
 
 lemma finite_def {a b : α} : finite a b ↔ ∃ n : ℕ, ¬a ^ (n + 1) ∣ b := iff.rfl
 
+lemma not_dvd_one_of_finite_one_right {a : α} : finite a 1 → ¬a ∣ 1 :=
+λ ⟨n, hn⟩ ⟨d, hd⟩, hn ⟨d ^ (n + 1), (pow_mul_pow_eq_one (n + 1) hd.symm).symm⟩
+
 @[norm_cast]
 theorem int.coe_nat_multiplicity (a b : ℕ) :
     multiplicity (a : ℤ) (b : ℤ) = multiplicity a b :=
@@ -61,14 +64,10 @@ lemma not_finite_iff_forall {a b : α} : (¬ finite a b) ↔ ∀ n : ℕ, a ^ n
   by simp [finite, multiplicity, not_not]; tauto⟩
 
 lemma not_unit_of_finite {a b : α} (h : finite a b) : ¬is_unit a :=
-let ⟨n, hn⟩ := h in mt (is_unit_iff_forall_dvd.1 ∘ is_unit.pow (n + 1)) $
-λ h, hn (h b)
-
-lemma finite_of_finite_mul_left {a b c : α} : finite a (b * c) → finite a c :=
-λ ⟨n, hn⟩, ⟨n, λ h, hn (h.trans (by simp [mul_pow]))⟩
+let ⟨n, hn⟩ := h in hn ∘ is_unit.dvd ∘ is_unit.pow (n + 1)
 
 lemma finite_of_finite_mul_right {a b c : α} : finite a (b * c) → finite a b :=
-by rw mul_comm; exact finite_of_finite_mul_left
+λ ⟨n, hn⟩, ⟨n, λ h, hn (h.trans (dvd_mul_right _ _))⟩
 
 variable [decidable_rel ((∣) : α → α → Prop)]
 
@@ -133,29 +132,19 @@ by { simp only [not_not],
      exact ⟨λ h n, nat.cases_on n (by { rw pow_zero, exact one_dvd _}) (λ n, h _), λ h n, h _⟩ }
 
 @[simp] lemma is_unit_left {a : α} (b : α) (ha : is_unit a) : multiplicity a b = ⊤ :=
-eq_top_iff.2 (λ _, is_unit_iff_forall_dvd.1 (ha.pow _) _)
-
-lemma is_unit_right {a b : α} (ha : ¬is_unit a) (hb : is_unit b) :
-  multiplicity a b = 0 :=
-eq_coe_iff.2 ⟨show a ^ 0 ∣ b, by simp only [pow_zero, one_dvd],
-  by { rw pow_one, exact λ h, mt (is_unit_of_dvd_unit h) ha hb }⟩
+eq_top_iff.2 (λ _, is_unit.dvd (ha.pow _))
 
 @[simp] lemma one_left (b : α) : multiplicity 1 b = ⊤ := is_unit_left b is_unit_one
 
-lemma one_right {a : α} (ha : ¬is_unit a) : multiplicity a 1 = 0 := is_unit_right ha is_unit_one
-
 @[simp] lemma get_one_right {a : α} (ha : finite a 1) : get (multiplicity a 1) ha = 0 :=
 begin
   rw [part_enat.get_eq_iff_eq_coe, eq_coe_iff, pow_zero],
-  simpa [is_unit_iff_dvd_one.symm] using not_unit_of_finite ha,
+  simp [not_dvd_one_of_finite_one_right ha],
 end
 
 @[simp] lemma unit_left (a : α) (u : αˣ) : multiplicity (u : α) a = ⊤ :=
 is_unit_left a u.is_unit
 
-lemma unit_right {a : α} (ha : ¬is_unit a) (u : αˣ) : multiplicity a u = 0 :=
-is_unit_right ha u.is_unit
-
 lemma multiplicity_eq_zero_of_not_dvd {a b : α} (ha : ¬a ∣ b) : multiplicity a b = 0 :=
 by { rw [← nat.cast_zero, eq_coe_iff], simpa }
 
@@ -192,14 +181,11 @@ lemma multiplicity_le_multiplicity_iff {a b c d : α} : multiplicity a b ≤ mul
     by rw [eq_top_iff_not_finite.2 hab, eq_top_iff_not_finite.2
       (not_finite_iff_forall.2 this)]⟩
 
-lemma multiplicity_le_multiplicity_of_dvd_left {a b c : α} (hdvd : a ∣ b) :
-  multiplicity b c ≤ multiplicity a c :=
-multiplicity_le_multiplicity_iff.2 $ λ n h, (pow_dvd_pow_of_dvd hdvd n).trans h
-
-lemma eq_of_associated_left {a b c : α} (h : associated a b) :
-  multiplicity b c = multiplicity a c :=
-le_antisymm (multiplicity_le_multiplicity_of_dvd_left h.dvd)
-  (multiplicity_le_multiplicity_of_dvd_left h.symm.dvd)
+lemma multiplicity_eq_multiplicity_iff {a b c d : α} : multiplicity a b = multiplicity c d ↔
+  (∀ n : ℕ, a ^ n ∣ b ↔ c ^ n ∣ d) :=
+⟨λ h n, ⟨multiplicity_le_multiplicity_iff.mp h.le n, multiplicity_le_multiplicity_iff.mp h.ge n⟩,
+ λ h, le_antisymm (multiplicity_le_multiplicity_iff.mpr (λ n, (h n).mp))
+                  (multiplicity_le_multiplicity_iff.mpr (λ n, (h n).mpr))⟩
 
 lemma multiplicity_le_multiplicity_of_dvd_right {a b c : α} (h : b ∣ c) :
   multiplicity a b ≤ multiplicity a c :=
@@ -240,11 +226,44 @@ end
 
 alias dvd_iff_multiplicity_pos ↔ _ _root_.has_dvd.dvd.multiplicity_pos
 
+end monoid
+
+section comm_monoid
+variables [comm_monoid α]
+
+lemma finite_of_finite_mul_left {a b c : α} : finite a (b * c) → finite a c :=
+by rw mul_comm; exact finite_of_finite_mul_right
+
+variable [decidable_rel ((∣) : α → α → Prop)]
+
+lemma is_unit_right {a b : α} (ha : ¬is_unit a) (hb : is_unit b) :
+  multiplicity a b = 0 :=
+eq_coe_iff.2 ⟨show a ^ 0 ∣ b, by simp only [pow_zero, one_dvd],
+  by { rw pow_one, exact λ h, mt (is_unit_of_dvd_unit h) ha hb }⟩
+
+lemma one_right {a : α} (ha : ¬is_unit a) : multiplicity a 1 = 0 := is_unit_right ha is_unit_one
+
+lemma unit_right {a : α} (ha : ¬is_unit a) (u : αˣ) : multiplicity a u = 0 :=
+is_unit_right ha u.is_unit
+
+open_locale classical
+
+lemma multiplicity_le_multiplicity_of_dvd_left {a b c : α} (hdvd : a ∣ b) :
+  multiplicity b c ≤ multiplicity a c :=
+multiplicity_le_multiplicity_iff.2 $ λ n h, (pow_dvd_pow_of_dvd hdvd n).trans h
+
+lemma eq_of_associated_left {a b c : α} (h : associated a b) :
+  multiplicity b c = multiplicity a c :=
+le_antisymm (multiplicity_le_multiplicity_of_dvd_left h.dvd)
+  (multiplicity_le_multiplicity_of_dvd_left h.symm.dvd)
+
+alias dvd_iff_multiplicity_pos ↔ _ _root_.has_dvd.dvd.multiplicity_pos
+
 end comm_monoid
 
-section comm_monoid_with_zero
+section monoid_with_zero
 
-variable [comm_monoid_with_zero α]
+variable [monoid_with_zero α]
 
 lemma ne_zero_of_finite {a b : α} (h : finite a b) : b ≠ 0 :=
 let ⟨n, hn⟩ := h in λ hb, by simpa [hb] using hn
@@ -260,6 +279,14 @@ begin
   rwa zero_dvd_iff,
 end
 
+end monoid_with_zero
+
+section comm_monoid_with_zero
+
+variable [comm_monoid_with_zero α]
+
+variable [decidable_rel ((∣) : α → α → Prop)]
+
 lemma multiplicity_mk_eq_multiplicity [decidable_rel ((∣) : associates α → associates α → Prop)]
   {a b : α} : multiplicity (associates.mk a) (associates.mk b) = multiplicity a b :=
 begin
@@ -274,15 +301,15 @@ begin
   { suffices : ¬ (finite (associates.mk a) (associates.mk b)),
     { rw [finite_iff_dom, part_enat.not_dom_iff_eq_top] at h this,
       rw [h, this] },
-    refine not_finite_iff_forall.mpr (λ n, by {rw [← associates.mk_pow, associates.mk_dvd_mk],
+    refine not_finite_iff_forall.mpr (λ n, by { rw [← associates.mk_pow, associates.mk_dvd_mk],
       exact not_finite_iff_forall.mp h n }) }
 end
 
 end comm_monoid_with_zero
 
-section comm_semiring
+section semiring
 
-variables [comm_semiring α] [decidable_rel ((∣) : α → α → Prop)]
+variables [semiring α] [decidable_rel ((∣) : α → α → Prop)]
 
 lemma min_le_multiplicity_add {p a b : α} :
   min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b) :=
@@ -292,13 +319,11 @@ lemma min_le_multiplicity_add {p a b : α} :
   (λ h, by rw [min_eq_right h, multiplicity_le_multiplicity_iff];
     exact λ n hn, dvd_add (multiplicity_le_multiplicity_iff.1 h n hn) hn)
 
-end comm_semiring
-
-section comm_ring
+end semiring
 
-variables [comm_ring α] [decidable_rel ((∣) : α → α → Prop)]
+section ring
 
-open_locale classical
+variables [ring α] [decidable_rel ((∣) : α → α → Prop)]
 
 @[simp] protected lemma neg (a b : α) : multiplicity a (-b) = multiplicity a b :=
 part.ext' (by simp only [multiplicity, part_enat.find, dvd_neg])
@@ -340,7 +365,7 @@ begin
   { rw [multiplicity_add_of_gt hab, min_eq_right], exact le_of_lt hab},
 end
 
-end comm_ring
+end ring
 
 section cancel_comm_monoid_with_zero
 
@@ -476,7 +501,6 @@ lemma multiplicity_pow_self_of_prime {p : α} (hp : prime p) (n : ℕ) :
   multiplicity p (p ^ n) = n :=
 multiplicity_pow_self hp.ne_zero hp.not_unit n
 
-
 end cancel_comm_monoid_with_zero
 
 section valuation