From e4e24a51453e9278559e9d355dff9f24b9ae5790 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 24 Nov 2023 10:23:13 +0000 Subject: [PATCH] feat: `m/gcd m n` and `n` coprime if `m` squarefree (#8578) --- Mathlib/Data/Nat/Squarefree.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean index 01babdb876609..cb49fb02d565c 100644 --- a/Mathlib/Data/Nat/Squarefree.lean +++ b/Mathlib/Data/Nat/Squarefree.lean @@ -392,6 +392,12 @@ theorem squarefree_mul_iff {m n : ℕ} : ⟨fun h => ⟨coprime_of_squarefree_mul h, (squarefree_mul $ coprime_of_squarefree_mul h).mp h⟩, fun h => (squarefree_mul h.1).mpr h.2⟩ +lemma coprime_div_gcd_of_squarefree (hm : Squarefree m) (hn : n ≠ 0) : Coprime (m / gcd m n) n := by + have : Coprime (m / gcd m n) (gcd m n) := + coprime_of_squarefree_mul $ by simpa [Nat.div_mul_cancel, gcd_dvd_left] + simpa [Nat.div_mul_cancel, gcd_dvd_right] using + (coprime_div_gcd_div_gcd (m := m) (gcd_ne_zero_right hn).bot_lt).mul_right this + lemma prod_primeFactors_of_squarefree (hn : Squarefree n) : ∏ p in n.primeFactors, p = n := by convert factorization_prod_pow_eq_self hn.ne_zero refine prod_congr rfl fun p hp ↦ ?_