multiplicity_factorial_pow — Mathlib

English

For a prime p, ν_p((p^n)!) = ∑_{i=0}^{n-1} p^i.

Русский

Для простого p: ν_p((p^n)!) = ∑_{i=0}^{n-1} p^i.

LaTeX

$$$ emultiplicity(p, (p^n)!) = \sum_{i=0}^{n-1} p^i $$$

Lean4

theorem multiplicity_factorial_pow {n p : ℕ} (hp : p.Prime) :
    multiplicity p (p ^ n).factorial = ∑ i ∈ Finset.range n, p ^ i :=
  by
  rw [← ENat.coe_inj, ← (Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, (p ^ n).factorial_pos⟩).emultiplicity_eq_multiplicity]
  induction n with
  | zero => simp [hp.emultiplicity_one]
  | succ n h => rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]

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