setOf_pow_dvd_eq_Icc_factorization

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]

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