English
Let m,n ∈ ℕ with gcd(m,n) = 1. Then Squarefree(m n) holds iff Squarefree(m) and Squarefree(n).
Русский
Пусть m,n ∈ ℕ и gcd(m,n) = 1. Тогда Squarefree(m n) выполняется тогда, когда Squarefree(m) и Squarefree(n).
LaTeX
$$$\\\\gcd(m,n)=1 \\\\Rightarrow \\\\operatorname{Squarefree}(m n) \\\\Longleftrightarrow \\\\operatorname{Squarefree}(m) \\\\land \\\\operatorname{Squarefree}(n).$$$
Lean4
/-- `Squarefree` is multiplicative. Note that the → direction does not require `hmn`
and generalizes to arbitrary commutative monoids. See `Squarefree.of_mul_left` and
`Squarefree.of_mul_right` above for auxiliary lemmas. -/
theorem squarefree_mul {m n : ℕ} (hmn : m.Coprime n) : Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n := by
simp [squarefree_mul_iff, Nat.coprime_iff_isRelPrime.mp hmn]
