Kummer’s theorem in MathComp

1.2 Binomial coefficients and factorials

Definition 1.7 Binomial coefficient
#

The binomial coefficient \(\binom {n}{k}\), written ’C(n, k) in MathComp.

Definition 1.8 Factorial
#

The factorial \(n!\), written n‘! in MathComp.

Lemma 1.9 Legendre’s formula

Let \(p\) be prime and \(n \in \mathbb {N}\). Then

\[ v_p(n!) = \sum _{k=1}^{n} \left\lfloor \frac{n}{p^k} \right\rfloor . \]

Lemma 1.10 Factorial decomposition of binomials

For \(k \leq n\),

\[ \binom {n}{k} \cdot k! \cdot (n-k)! = n!. \]

Lemma 1.11 Positivity of binomial coefficients
#

\((0 {\lt} \binom {n}{k}) \iff (k \leq n)\).

Lemma 1.12 Positivity of factorial
#

\(0 {\lt} n!\) for all \(n\).