padicValNat_mul_div_factorial — Mathlib

English

For primes p ≠ q, v_q(p^n q^m) = m.

Русский

Для простых p ≠ q верно v_q(p^n q^m) = m.

LaTeX

$$$\\forall p,q,n,m \\in \\mathbb{N},\\ p,q\\text{ primes},\\ q \\neq p \\Rightarrow \\operatorname{padicValNat}(q, p^n \\cdot q^m)=m$$$

Lean4

/-- The `p`-adic valuation of `n!` is equal to the `p`-adic valuation of the factorial of the
largest multiple of `p` below `n`, i.e. `(p * ⌊n / p⌋)!`. -/
@[simp]
theorem padicValNat_mul_div_factorial (n : ℕ) [hp : Fact p.Prime] : padicValNat p (p * (n / p))! = padicValNat p n ! :=
  by
  nth_rw 2 [← div_add_mod n p]
  exact (padicValNat_factorial_mul_add (n / p) <| mod_lt n hp.out.pos).symm

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