Theorems · Theorem · number theory

padicValNat_choose

∀ {p n k b : ℕ} [hp : Fact (Nat.Prime p)],
  k ≤ n → Nat.log p n < b → padicValNat p (n.choose k) = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card

Kummer's Theorem The p-adic valuation of n.choose k is the number of carries when k and n - k are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

Defined in

Mathlib.NumberTheory.Padics.PadicVal.Basic

Cited by

0 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact