factorization_eq_card_pow_dvd — Mathlib

English

For any n with a prime p, the p-adic valuation of n is the count of i with p^i | n, i.e., the p-th coefficient in the factorization equals the cardinality of the corresponding subset of exponents.

Русский

Для любого n и простого p показатель p в факторизации n равен количеству i, таких что p^i делит n; т.е. показатель p в факторизации равно мощности соответствующего множества степеней.

LaTeX

$$$ n.factorization p = #\{ i \in \mathrm{Ico}(1, n) \mid p^i \mid n \}$$$

Lean4

theorem factorization_eq_card_pow_dvd (n : ℕ) {p : ℕ} (pp : p.Prime) :
    n.factorization p = #({i ∈ Ico 1 n | p ^ i ∣ n}) := by simp [← Icc_factorization_eq_pow_dvd n pp]

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