Source indexedlemma · leanprover/lean4:v4.32.0

MobiusLemma.sq_dvd_mul_iff_of_coprime

PrimeNumberTheoremAnd.IEANTN.MobiusLemma · PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean:49 to 58

Source documentation

If m, n are coprime and a ∣ m, b ∣ n, then (ab)² ∣ mn iff a² ∣ m and b² ∣ n.

Exact Lean statement

lemma sq_dvd_mul_iff_of_coprime {m n a b : ℕ} (hmn : m.Coprime n) (ha : a ∣ m) (hb : b ∣ n) :
    (a * b) ^ 2 ∣ m * n ↔ a ^ 2 ∣ m ∧ b ^ 2 ∣ n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sq_dvd_mul_iff_of_coprime {m n a b : ℕ} (hmn : m.Coprime n) (ha : a ∣ m) (hb : b ∣ n) :    (a * b) ^ 2 ∣ m * n ↔ a ^ 2 ∣ m ∧ b ^ 2 ∣ n := by  refine ⟨fun h ↦ ?_, fun ⟨ha', hb'⟩ ↦ ?_⟩  · rw [mul_pow] at h    constructor    · exact ((hmn.coprime_dvd_left ha).pow_left 2).dvd_of_dvd_mul_right        ((dvd_mul_right _ _).trans h)    · exact ((hmn.coprime_dvd_right hb).symm.pow_left 2).dvd_of_dvd_mul_left        ((dvd_mul_left _ _).trans h)  · rw [mul_pow ..]; exact mul_dvd_mul ha' hb'