English
Two squarefree numbers n and m are equal iff the set of primes dividing n and m coincide.
Русский
Два квадратносвободных числа n и m равны тогда и только тогда, когда множества простых делителей совпадают.
LaTeX
$$$n,m \\ge 0, Squarefree(n) \\land Squarefree(m) \\rightarrow (n = m \\iff \\forall p, Prime(p) \\rightarrow (p \\mid n \\iff p \\mid m))$$$
Lean4
theorem ext_iff {n m : ℕ} (hn : Squarefree n) (hm : Squarefree m) : n = m ↔ ∀ p, Prime p → (p ∣ n ↔ p ∣ m) :=
by
refine ⟨by rintro rfl; simp, fun h => eq_of_factorization_eq hn.ne_zero hm.ne_zero fun p => ?_⟩
by_cases hp : p.Prime
· have h₁ := h _ hp
rw [← not_iff_not, hp.dvd_iff_one_le_factorization hn.ne_zero, not_le, lt_one_iff,
hp.dvd_iff_one_le_factorization hm.ne_zero, not_le, lt_one_iff] at h₁
have h₂ := hn.natFactorization_le_one p
have h₃ := hm.natFactorization_le_one p
cutsat
rw [factorization_eq_zero_of_non_prime _ hp, factorization_eq_zero_of_non_prime _ hp]
