Email Gateway (Aug 23 2022 at 09:00): Email Gateway (Aug 23 2022 at 09:00):From: Manuel Eberl <eberlm@in.tum.de>
Lucas's Theorem
by Chelsea Edmonds
This work presents a formalisation of a generating function proof for
Lucas's theorem. We first outline extensions to the existing Formal
Power Series (FPS) library, including an equivalence relation for
coefficients modulo n, an alternate binomial theorem statement, and a
formalised proof of the Freshman's dream (mod p) lemma. The second part
of the work presents the formal proof of Lucas's Theorem. Working
backwards, the formalisation first proves a well known corollary of the
theorem which is easier to formalise, and then applies induction to
prove the original theorem statement. The proof of the corollary aims to
provide a good example of a formalised generating function equivalence
proof using the FPS library. The final theorem statement is intended to
be integrated into the formalised proof of Hilbert's 10th Problem.
https://www.isa-afp.org/entries/Lucas_Theorem.html
Enjoy!
Manuel
Last updated: Apr 24 2024 at 20:16 UTC