squarefree_mul_iff — Mathlib

English

For all m,n ∈ ℕ, Squarefree(m n) holds iff m and n are coprime and both squarefree.

Русский

Для любых m,n ∈ ℕ Squarefree(m n) выполняется тогда и только тогда, когда m и n взаимно просты и оба квадратно свободны.

LaTeX

$$$\\\\operatorname{Squarefree}(m n) \\\\iff (m \\perp n) \\\\land \\\\operatorname{Squarefree}(m) \\\\land \\\\operatorname{Squarefree}(n).$$$

Lean4

theorem squarefree_mul_iff {m n : ℕ} : Squarefree (m * n) ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n := by
  rw [_root_.squarefree_mul_iff, Nat.coprime_iff_isRelPrime]

Похожие утверждения