English
If n is squarefree, then for every p, the exponent of p in the factorization of n is at most 1.
Русский
Если n квадратносвободноe, то для каждого p степень p в факторизации n не превосходит единицы.
LaTeX
$$$\\forall p, \\text{Squarefree}(n) \\rightarrow n.factorization(p) \\le 1$$$
Lean4
theorem _root_.Squarefree.natFactorization_le_one {n : ℕ} (p : ℕ) (hn : Squarefree n) : n.factorization p ≤ 1 :=
by
rcases eq_or_ne n 0 with (rfl | hn')
· simp
rw [squarefree_iff_emultiplicity_le_one] at hn
by_cases hp : p.Prime
· have := hn p
rw [← multiplicity_eq_factorization hp hn']
simp only [Nat.isUnit_iff, hp.ne_one, or_false] at this
exact multiplicity_le_of_emultiplicity_le this
· rw [factorization_eq_zero_of_non_prime _ hp]
exact zero_le_one
