padicValNat_factorial_mul_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem padicValNat_factorial_mul_add {n : ℕ} (m : ℕ) [hp : Fact p.Prime] (h : n < p) :
    padicValNat p (p * m + n)! = padicValNat p (p * m)! := by
  induction n with
  | zero => rw [add_zero]
  | succ n hn =>
    rw [add_succ, factorial_succ, padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo
        ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
          (Nat.mul_add _ _ _ ▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]

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