mathlib

41a820dd - feat(number_theory/lucas_primality): Add theorem for Lucas primality test (#8820)

feat(number_theory/lucas_primality): Add theorem for Lucas primality test (#8820) This is a PR for adding the [Lucas primality test](https://en.wikipedia.org/wiki/Lucas_primality_test) to mathlib. This tells us that a number `p` is prime when an element `a : zmod p` has order `p-1` . Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>