Binomial coefficients modulo a prime and p-adic valuation #
The binomial coefficient at p ^ v_p(e) stays nonzero modulo p when its upper argument is
any natural number congruent to nonzero e modulo a sufficiently large power of p.
theorem
TauCeti.natCast_choose_pow_padicValInt_ne_zero_of_modEq
{p : ℕ}
[Fact (Nat.Prime p)]
{e : ℤ}
(he : e ≠ 0)
{K : ℕ}
(hK : padicValInt p e < K)
{n : ℕ}
(hn : ↑n ≡ e [ZMOD ↑p ^ K])
:
If K exceeds v_p(e) for nonzero e, then for every natural number n congruent to
e modulo p ^ K, the binomial coefficient n.choose (p ^ v_p(e)) is nonzero modulo p.