Theorems · Theorem · number theory

Nat.Prime.emultiplicity_choose

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

The multiplicity of p in choose n k is the number of carries when k and n - k are added in base p. The set is expressed by filtering Ico 1 b where b is any bound greater than log p n.

Defined in

Mathlib.Data.Nat.Multiplicity

Cited by

2 results in Mathlib

Foundations

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