[Merged by Bors] - feat: add some Associated/Prime lemmas

Mathlib/Algebra/Associated.lean

@@ -48,6 +48,12 @@ theorem dvd_or_dvd (hp : Prime p) {a b : α} (h : p ∣ a * b) : p ∣ a ∨ p 
   hp.2.2 a b h
 #align prime.dvd_or_dvd Prime.dvd_or_dvd
 
+theorem dvd_mul {a b : α} : p ∣ a * b ↔ p ∣ a ∨ p ∣ b :=
+  ⟨hp.dvd_or_dvd, (Or.elim · (dvd_mul_of_dvd_left · _) (dvd_mul_of_dvd_right · _))⟩
+
+theorem not_dvd_mul {a b : α} (ha : ¬ p ∣ a) (hb : ¬ p ∣ b) : ¬ p ∣ a * b :=
+  hp.dvd_mul.not.mpr <| not_or.mpr ⟨ha, hb⟩
+
 theorem dvd_of_dvd_pow (hp : Prime p) {a : α} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a := by
   induction' n with n ih
   · rw [pow_zero] at h
@@ -60,11 +66,8 @@ theorem dvd_of_dvd_pow (hp : Prime p) {a : α} {n : ℕ} (h : p ∣ a ^ n) : p 
   exact ih dvd_pow
 #align prime.dvd_of_dvd_pow Prime.dvd_of_dvd_pow
 
-theorem dvd_mul {a b : α} : p ∣ a * b ↔ p ∣ a ∨ p ∣ b :=
-  ⟨hp.dvd_or_dvd, (Or.elim · (dvd_mul_of_dvd_left · _) (dvd_mul_of_dvd_right · _))⟩
-
-theorem not_dvd_mul {a b : α} (ha : ¬ p ∣ a) (hb : ¬ p ∣ b) : ¬ p ∣ a * b :=
-  hp.dvd_mul.not.mpr <| not_or.mpr ⟨ha, hb⟩
+theorem dvd_pow_iff_dvd {a : α} {n : ℕ} (hn : n ≠ 0) : p ∣ a ^ n ↔ p ∣ a :=
+  ⟨hp.dvd_of_dvd_pow, (dvd_pow · hn)⟩
 
 end Prime
 

Mathlib/Algebra/BigOperators/Associated.lean

@@ -57,6 +57,19 @@ theorem Prod.associated_iff {M N : Type*} [Monoid M] [Monoid N] {x z : M × N} :
   fun ⟨⟨u₁, h₁⟩, ⟨u₂, h₂⟩⟩ =>
     ⟨MulEquiv.prodUnits.invFun (u₁, u₂), Prod.eq_iff_fst_eq_snd_eq.2 ⟨h₁, h₂⟩⟩⟩
 
+theorem Associated.prod {M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι) (f : ι → M)
+    (g : ι → M) (h : ∀ i, i ∈ s → Associated (f i) (g i)) : (∏ i in s, f i) ~ᵤ (∏ i in s, g i) := by
+  induction s using Finset.induction with
+  | empty =>
+    simp only [Finset.prod_empty]
+    rfl
+  | @insert j s hjs IH =>
+    classical
+    convert_to Associated (∏ i in insert j s, f i) (∏ i in insert j s, g i)
+    rw [Finset.prod_insert hjs, Finset.prod_insert hjs]
+    exact Associated.mul_mul (h j (Finset.mem_insert_self j s))
+      (IH (fun i hi ↦ h i (Finset.mem_insert_of_mem hi)))
+
 theorem exists_associated_mem_of_dvd_prod [CancelCommMonoidWithZero α] {p : α} (hp : Prime p)
     {s : Multiset α} : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
   Multiset.induction_on s (by simp [mt isUnit_iff_dvd_one.2 hp.not_unit]) fun a s ih hs hps => by

Mathlib/Algebra/Ring/Units.lean

@@ -101,6 +101,8 @@ theorem IsUnit.neg_iff [Monoid α] [HasDistribNeg α] (a : α) : IsUnit (-a) ↔
   ⟨fun h => neg_neg a ▸ h.neg, IsUnit.neg⟩
 #align is_unit.neg_iff IsUnit.neg_iff
 
+theorem isUnit_neg_one [Monoid α] [HasDistribNeg α] : IsUnit (-1 : α) := isUnit_one.neg
+
 theorem IsUnit.sub_iff [Ring α] {x y : α} : IsUnit (x - y) ↔ IsUnit (y - x) :=
   (IsUnit.neg_iff _).symm.trans <| neg_sub x y ▸ Iff.rfl
 #align is_unit.sub_iff IsUnit.sub_iff