From 9017045d80ba815ed0a08dbe6ccf9ff2cb75a46f Mon Sep 17 00:00:00 2001 From: NoahW314 Date: Sat, 23 May 2026 21:47:09 -0600 Subject: [PATCH 1/2] add `mul_dvd_left_iff_isUnit` --- Mathlib/Algebra/GroupWithZero/Divisibility.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Algebra/GroupWithZero/Divisibility.lean b/Mathlib/Algebra/GroupWithZero/Divisibility.lean index 4a2d08613d6ba2..8976ee9021db88 100644 --- a/Mathlib/Algebra/GroupWithZero/Divisibility.lean +++ b/Mathlib/Algebra/GroupWithZero/Divisibility.lean @@ -172,6 +172,15 @@ lemma pow_dvd_pow_iff (ha₀ : a ≠ 0) (ha : ¬IsUnit a) : a ^ n ∣ a ^ m ↔ apply pow_ne_zero m ha₀ · apply pow_dvd_pow +lemma mul_dvd_left_iff_isUnit {a b : α} (ha0 : a ≠ 0) : a * b ∣ a ↔ IsUnit b := by + nth_rw 2 [← mul_one a] + rw [mul_dvd_mul_iff_left ha0] + exact isUnit_iff_dvd_one.symm + +lemma mul_dvd_right_iff_isUnit {a b : α} (ha0 : a ≠ 0) : b * a ∣ a ↔ IsUnit b := by + rw [mul_comm] + exact mul_dvd_left_iff_isUnit ha0 + end CancelCommMonoidWithZero section GroupWithZero From 1dbc55793abc6c9a3e248782b495f70412f8e534 Mon Sep 17 00:00:00 2001 From: NoahW314 Date: Sat, 23 May 2026 21:47:46 -0600 Subject: [PATCH 2/2] Update Divisibility.lean --- Mathlib/Algebra/GroupWithZero/Divisibility.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/GroupWithZero/Divisibility.lean b/Mathlib/Algebra/GroupWithZero/Divisibility.lean index 8976ee9021db88..125c825a858482 100644 --- a/Mathlib/Algebra/GroupWithZero/Divisibility.lean +++ b/Mathlib/Algebra/GroupWithZero/Divisibility.lean @@ -172,12 +172,12 @@ lemma pow_dvd_pow_iff (ha₀ : a ≠ 0) (ha : ¬IsUnit a) : a ^ n ∣ a ^ m ↔ apply pow_ne_zero m ha₀ · apply pow_dvd_pow -lemma mul_dvd_left_iff_isUnit {a b : α} (ha0 : a ≠ 0) : a * b ∣ a ↔ IsUnit b := by +lemma mul_dvd_left_iff_isUnit (ha0 : a ≠ 0) : a * b ∣ a ↔ IsUnit b := by nth_rw 2 [← mul_one a] rw [mul_dvd_mul_iff_left ha0] exact isUnit_iff_dvd_one.symm -lemma mul_dvd_right_iff_isUnit {a b : α} (ha0 : a ≠ 0) : b * a ∣ a ↔ IsUnit b := by +lemma mul_dvd_right_iff_isUnit (ha0 : a ≠ 0) : b * a ∣ a ↔ IsUnit b := by rw [mul_comm] exact mul_dvd_left_iff_isUnit ha0