padicValNat_factorial_mul — Mathlib

English

The p-adic valuation of (p n)! equals the p-adic valuation of n! plus n.

Русский

p-адическая оценка (p n)! равна p-адической оценке n! плюс n.

LaTeX

$$$\\operatorname{padicValNat}(p, (p \\cdot n)!) = \\operatorname{padicValNat}(p, n!) + n$$$

Lean4

/-- The `p`-adic valuation of `(p * n)!` is `n` more than that of `n!`. -/
theorem padicValNat_factorial_mul (n : ℕ) [hp : Fact p.Prime] : padicValNat p (p * n)! = padicValNat p n ! + n :=
  by
  apply Nat.cast_injective (R := ℕ∞)
  rw [padicValNat_eq_emultiplicity <| factorial_ne_zero (p * n), Nat.cast_add,
    padicValNat_eq_emultiplicity <| factorial_ne_zero n]
  exact Prime.emultiplicity_factorial_mul hp.out

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