Binomial_Coefficient_involving_Power_of_Prime
Provedbinomial-coefficientsprime-numbersproofwiki
C(p^n * k, p^n) ≡ k (mod p).
Preamble
import Mathlib.Data.ZMod.Basic import Mathlib.Data.Nat.Choose.Factorization
Formal statement
theorem Binomial_Coefficient_involving_Power_of_Prime (p : ℕ) (hp : Nat.Prime p) (n k : ℕ) : (Nat.choose (p ^ n * k) (p ^ n) : ZMod p) = (k : ZMod p) := by sorry
Source