English
Let p be prime and n > 0. The set of positive integers i with p^i dividing n equals the interval 1 ≤ i ≤ v_p(n), i.e., Icc(1, n.factorization p).
Русский
Пусть p — простое и n > 0. Тогда множество положительных степеней i, для которых p^i делит n, равно отрезку 1 ≤ i ≤ v_p(n), то есть Icc(1, n.factorization p).
LaTeX
$$$ \{ i \in \mathbb{N} \mid i \neq 0 \land p^i \mid n \} = \mathrm{Icc}(1, n.factorization\, p) $$$
Lean4
theorem setOf_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) :
{i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (n.factorization p) :=
by
ext
simp [one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn]