Commit 2021-11-05 00:43 41a820dd

View on Github →

feat(number_theory/lucas_primality): Add theorem for Lucas primality test (#8820) This is a PR for adding the Lucas primality test to mathlib. This tells us that a number p is prime when an element a : zmod p has order p-1 .

Estimated changes

Modified src/algebra/divisibility.lean

added theorem dvd_iff_exists_eq_mul_left

Modified src/data/nat/totient.lean

added theorem nat.card_units_zmod_lt_sub_one

added theorem nat.prime_iff_card_units

added theorem nat.totient_lt

modified theorem zmod.card_units_eq_totient

Modified src/group_theory/order_of_element.lean

added theorem order_of_eq_of_pow_and_pow_div_prime

Created src/number_theory/lucas_primality.lean

added theorem lucas_primality