Commit 2023-04-15 00:49 94f9f7af

View on Github →

feat: port NumberTheory.LucasLehmer (#2988) This generalizes some results from LeftCancelMonoid to work around an issue in LucasLehmer.order_ineq.

Estimated changes

modified theorem pow_inj_mod
modified theorem pow_injective_of_lt_orderOf
added theorem LucasLehmer.X.add_fst
added theorem LucasLehmer.X.add_snd
added theorem LucasLehmer.X.card_eq
added theorem LucasLehmer.X.coe_mul
added theorem LucasLehmer.X.coe_nat
added theorem LucasLehmer.X.ext
added theorem LucasLehmer.X.mul_fst
added theorem LucasLehmer.X.mul_snd
added theorem LucasLehmer.X.neg_fst
added theorem LucasLehmer.X.neg_snd
added theorem LucasLehmer.X.one_fst
added theorem LucasLehmer.X.one_snd
added theorem LucasLehmer.X.zero_fst
added theorem LucasLehmer.X.zero_snd
added def LucasLehmer.X.ω
added def LucasLehmer.X
added theorem LucasLehmer.order_ineq
added theorem LucasLehmer.order_ω
added def LucasLehmer.q
added def LucasLehmer.s
added def LucasLehmer.sMod
added theorem LucasLehmer.sMod_lt
added theorem LucasLehmer.sMod_mod
added theorem LucasLehmer.sMod_succ
added theorem LucasLehmer.sZMod_eq_s
added theorem LucasLehmer.two_lt_q
added theorem LucasLehmer.ωUnit_coe
added def mersenne
added theorem mersenne_pos
added theorem modEq_mersenne
added theorem one_lt_mersenne
added theorem succ_mersenne