Ideas for proving this number theory lemma

Stream: new members

[Roshan Kohli]

lemma binomial_coeff_div {n m : ℕ} (hp : Nat.gcd m p = 1) : Nat.choose (m * p ^ n) (p ^ n) ≡ m [MOD p] := by

I am trying to prove this lemma in lean. I have attempted to do it directly however I know I can prove this by considering the polynomial $1+X^p$ over the finite field of p elements. But I have no clue on to even get started in that direction. Any advice would be appreciated. Thanks!

[Kevin Buzzard]

Are you sure you need hp?

I would prove it by induction on n.

[Roshan Kohli]

okay i'll give that a go

[Joël Riou]

It seems to me the formula is the particular case i = 1 for the congruence Nat.choose (m * p ^ n) (i * p ^ n) ≡ Nat.choose m i [MOD p]. If I had to prove the particular case, I would try to prove the more general case (which itself seems to be a special case of Lucas's theorem), which I would do by studying powers of 1+X in polynomial algebras over rings where the prime number p vanishes (but I do not know enough of the internals of mathlib for this area of mathematics...).