feat: add gcd_neg, neg_gcd (#12593)

Author: Ruben-VandeVelde

Mathlib/Algebra/Associated.lean

@@ -403,6 +403,9 @@ protected theorem refl [Monoid α] (x : α) : x ~ᵤ x :=
   ⟨1, by simp⟩
 #align associated.refl Associated.refl
 
+protected theorem rfl [Monoid α] {x : α} : x ~ᵤ x :=
+  .refl x
+
 instance [Monoid α] : IsRefl α Associated :=
   ⟨Associated.refl⟩
 
@@ -561,6 +564,9 @@ protected theorem Associated.dvd [Monoid α] {a b : α} : a ~ᵤ b → a ∣ b :
   ⟨u, hu.symm⟩
 #align associated.dvd Associated.dvd
 
+protected theorem Associated.dvd' [Monoid α] {a b : α} (h : a ~ᵤ b) : b ∣ a :=
+  h.symm.dvd
+
 protected theorem Associated.dvd_dvd [Monoid α] {a b : α} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a :=
   ⟨h.dvd, h.symm.dvd⟩
 #align associated.dvd_dvd Associated.dvd_dvd
@@ -608,6 +614,18 @@ theorem Associated.ne_zero_iff [MonoidWithZero α] {a b : α} (h : a ~ᵤ b) : a
   not_congr h.eq_zero_iff
 #align associated.ne_zero_iff Associated.ne_zero_iff
 
+theorem Associated.neg_left [Monoid α] [HasDistribNeg α] {a b : α} (h : Associated a b) :
+    Associated (-a) b :=
+  let ⟨u, hu⟩ := h; ⟨-u, by simp [hu]⟩
+
+theorem Associated.neg_right [Monoid α] [HasDistribNeg α] {a b : α} (h : Associated a b) :
+    Associated a (-b) :=
+  h.symm.neg_left.symm
+
+theorem Associated.neg_neg [Monoid α] [HasDistribNeg α] {a b : α} (h : Associated a b) :
+    Associated (-a) (-b) :=
+  h.neg_left.neg_right
+
 protected theorem Associated.prime [CommMonoidWithZero α] {p q : α} (h : p ~ᵤ q) (hp : Prime p) :
     Prime q :=
   ⟨h.ne_zero_iff.1 hp.ne_zero,

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -191,6 +191,11 @@ theorem dvd_antisymm_of_normalize_eq {a b : α} (ha : normalize a = a) (hb : nor
   ha ▸ hb ▸ normalize_eq_normalize hab hba
 #align dvd_antisymm_of_normalize_eq dvd_antisymm_of_normalize_eq
 
+theorem Associated.eq_of_normalized
+    {a b : α} (h : Associated a b) (ha : normalize a = a) (hb : normalize b = b) :
+    a = b :=
+  dvd_antisymm_of_normalize_eq ha hb h.dvd h.dvd'
+
 --can be proven by simp
 theorem dvd_normalize_iff {a b : α} : a ∣ normalize b ↔ a ∣ b :=
   Units.dvd_mul_right
@@ -435,6 +440,11 @@ theorem gcd_dvd_gcd [GCDMonoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d
   dvd_gcd ((gcd_dvd_left _ _).trans hab) ((gcd_dvd_right _ _).trans hcd)
 #align gcd_dvd_gcd gcd_dvd_gcd
 
+protected theorem Associated.gcd [GCDMonoid α]
+    {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) :
+    Associated (gcd a₁ b₁) (gcd a₂ b₂) :=
+  associated_of_dvd_dvd (gcd_dvd_gcd ha.dvd hb.dvd) (gcd_dvd_gcd ha.dvd' hb.dvd')
+
 @[simp]
 theorem gcd_same [NormalizedGCDMonoid α] (a : α) : gcd a a = normalize a :=
   gcd_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_refl a))
@@ -714,6 +724,24 @@ theorem Irreducible.gcd_eq_one_iff [NormalizedGCDMonoid α] {x y : α} (hx : Irr
     gcd x y = 1 ↔ ¬(x ∣ y) := by
   rw [← hx.isUnit_gcd_iff, ← normalize_eq_one, NormalizedGCDMonoid.normalize_gcd]
 
+section Neg
+
+variable [HasDistribNeg α]
+
+lemma gcd_neg' [GCDMonoid α] {a b : α} : Associated (gcd a (-b)) (gcd a b) :=
+  Associated.gcd .rfl (.neg_left .rfl)
+
+lemma gcd_neg [NormalizedGCDMonoid α] {a b : α} : gcd a (-b) = gcd a b :=
+  gcd_neg'.eq_of_normalized (normalize_gcd _ _) (normalize_gcd _ _)
+
+lemma neg_gcd' [GCDMonoid α] {a b : α} : Associated (gcd (-a) b) (gcd a b) :=
+  Associated.gcd (.neg_left .rfl) .rfl
+
+lemma neg_gcd [NormalizedGCDMonoid α] {a b : α} : gcd (-a) b = gcd a b :=
+  neg_gcd'.eq_of_normalized (normalize_gcd _ _) (normalize_gcd _ _)
+
+end Neg
+
 end GCD
 
 section LCM
@@ -799,6 +827,11 @@ theorem lcm_dvd_lcm [GCDMonoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d
   lcm_dvd (hab.trans (dvd_lcm_left _ _)) (hcd.trans (dvd_lcm_right _ _))
 #align lcm_dvd_lcm lcm_dvd_lcm
 
+protected theorem Associated.lcm [GCDMonoid α]
+    {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) :
+    Associated (lcm a₁ b₁) (lcm a₂ b₂) :=
+  associated_of_dvd_dvd (lcm_dvd_lcm ha.dvd hb.dvd) (lcm_dvd_lcm ha.dvd' hb.dvd')
+
 @[simp]
 theorem lcm_units_coe_left [NormalizedGCDMonoid α] (u : αˣ) (a : α) : lcm (↑u) a = normalize a :=
   lcm_eq_normalize (lcm_dvd Units.coe_dvd dvd_rfl) (dvd_lcm_right _ _)
@@ -1424,16 +1457,6 @@ theorem normalize_eq_one {a : G₀} (h0 : a ≠ 0) : normalize a = 1 := by simp
 
 end CommGroupWithZero
 
-theorem Associated.gcd [CancelCommMonoidWithZero α] [GCDMonoid α]
-    {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) :
-    Associated (gcd a₁ b₁) (gcd a₂ b₂) :=
-  associated_of_dvd_dvd (gcd_dvd_gcd ha.dvd hb.dvd) (gcd_dvd_gcd ha.symm.dvd hb.symm.dvd)
-
-theorem Associated.lcm [CancelCommMonoidWithZero α] [GCDMonoid α]
-    {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) :
-    Associated (lcm a₁ b₁) (lcm a₂ b₂) :=
-  associated_of_dvd_dvd (lcm_dvd_lcm ha.dvd hb.dvd) (lcm_dvd_lcm ha.symm.dvd hb.symm.dvd)
-
 namespace Associates
 
 variable [CancelCommMonoidWithZero α] [GCDMonoid α]