Commit 2024-07-23 14:14 15fee0ab

feat(Data/Nat/Choose): Lucas' theorem (#8612) This PR proves Lucas' theorem, which states that $\binom{n}{k} \equiv \prod_i \binom{\lfloor n / p^i \rfloor \pmod{p}}{\lfloor k / p^i \rfloor \pmod{p}} \equiv \prod_i \binom{n_i}{k_i} \pmod{p}$, where $n_i$ and $k_i$ are the $i$-th base-$p$ digits of $n$ and $k$ respectively. This is proven by looking at Freshman's dream closely + induction