From b46688d68312ff2926af89deae1cfe0523b5cd41 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Mon, 5 Jan 2026 13:12:50 +1000 Subject: [PATCH] feat: add `Nat.gcd_left_comm` and `Int.gcd_left_comm` (#11901) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds `gcd_left_comm` lemmas for both `Nat` and `Int`: - `Nat.gcd_left_comm`: `gcd m (gcd n k) = gcd n (gcd m k)` - `Int.gcd_left_comm`: `gcd a (gcd b c) = gcd b (gcd a c)` These lemmas establish the left-commutativity property for gcd, complementing the existing `gcd_comm` and `gcd_assoc` lemmas. Upstreamed from https://github.com/leanprover-community/mathlib4/pull/33235 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.5 --- src/Init/Data/Int/Gcd.lean | 2 ++ src/Init/Data/Nat/Gcd.lean | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/Init/Data/Int/Gcd.lean b/src/Init/Data/Int/Gcd.lean index 913c857fef..49f3b2027d 100644 --- a/src/Init/Data/Int/Gcd.lean +++ b/src/Init/Data/Int/Gcd.lean @@ -113,6 +113,8 @@ theorem gcd_eq_right_iff_dvd (hb : 0 ≤ b) : gcd a b = b ↔ b ∣ a := by theorem gcd_assoc (a b c : Int) : gcd (gcd a b) c = gcd a (gcd b c) := Nat.gcd_assoc .. +theorem gcd_left_comm (a b c : Int) : gcd a (gcd b c) = gcd b (gcd a c) := Nat.gcd_left_comm .. + theorem gcd_mul_left (m n k : Int) : gcd (m * n) (m * k) = m.natAbs * gcd n k := by simp [gcd_eq_natAbs_gcd_natAbs, Nat.gcd_mul_left, natAbs_mul] diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean index 7a1a573ea8..60ef917ea4 100644 --- a/src/Init/Data/Nat/Gcd.lean +++ b/src/Init/Data/Nat/Gcd.lean @@ -129,6 +129,9 @@ theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) := (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k))) instance : Std.Associative gcd := ⟨gcd_assoc⟩ +theorem gcd_left_comm (m n k : Nat) : gcd m (gcd n k) = gcd n (gcd m k) := by + rw [← gcd_assoc, ← gcd_assoc, gcd_comm m n] + @[simp] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n) theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k := by