LucasLehmer

📁 Source: Mathlib/NumberTheory/LucasLehmer.lean

Statistics

Metric	Count
Definitions LucasLehmerTest, X, instAddCommGroup, instAddGroupWithOne, instCoeZMod, instCommRing, instDecidableEq, instFintype, instInhabited, instMonoid, instMul, instNatCast, instOne, instRing, α, ω, ωb, lucasLehmerResidue, evalLucasLehmerTest, sModNat, sModNatTR, sModNat_aux, q, s, sMod, sZMod, ωUnit, evalMersenne, mersenne	29
Theorems add_fst, add_snd, card_eq, card_units_lt, closed_form, coe_mul, coe_natCast, ext, ext_iff, fst_intCast, fst_natCast, instCharP, instNontrivialOfFactLtNatOfNat, left_distrib, mul_fst, mul_snd, neg_fst, neg_snd, ofNat_fst, ofNat_snd, one_add_α_pow_q, one_add_α_pow_q_succ, one_add_α_sq, one_fst, one_snd, pow_ω, right_distrib, snd_intCast, snd_natCast, two_mul_ω_pow, zero_fst, zero_snd, α_pow, α_sq, ω_mul_ωb, ω_pow_trace, ωb_mul_ω, mersenne_coe_X, mersenne_int_ne_zero, mersenne_int_pos, isNat_lucasLehmerTest, isNat_not_lucasLehmerTest, sModNatTR_eq_sModNat, sModNat_aux_eq, sModNat_eq_sMod, testFalseHelper, testTrueHelper, order_ineq, order_ω, residue_eq_zero_iff_sMod_eq_zero, sMod_lt, sMod_mod, sMod_nonneg, sZMod_eq_s, sZMod_eq_sMod, two_lt_q, ωUnit_coe, ω_pow_eq_neg_one, ω_pow_eq_one, ω_pow_formula, mersenne_pos_of_pos, of_mersenne, legendreSym_mersenne_three, legendreSym_mersenne_two, lucas_lehmer_necessity, lucas_lehmer_sufficiency, mersenne_le_mersenne, mersenne_lt_mersenne, mersenne_mod_eight, mersenne_mod_four, mersenne_mod_three, mersenne_odd, mersenne_pos, mersenne_succ, mersenne_zero, modEq_mersenne, one_lt_mersenne, strictMono_mersenne, succ_mersenne	79
Total	108

LucasLehmer

Definitions

Name	Category	Theorems
LucasLehmerTest 📖	MathDef	3 math math: norm_num_ext.testTrueHelper, lucas_lehmer_necessity, norm_num_ext.testFalseHelper
X 📖	CompOp	39 math math: X.fst_natCast, mersenne_coe_X, X.two_mul_ω_pow, X.card_eq, X.zero_fst, X.neg_snd, X.instNontrivialOfFactLtNatOfNat, X.one_add_α_sq, X.one_add_α_pow_q_succ, X.ωb_mul_ω, X.right_distrib, X.α_pow, X.card_units_lt, ω_pow_eq_one, X.closed_form, X.left_distrib, X.add_snd, X.one_fst, X.coe_natCast, X.mul_fst, X.instCharP, X.ω_pow_trace, X.snd_intCast, ωUnit_coe, X.add_fst, order_ω, X.ω_mul_ωb, X.mul_snd, X.α_sq, X.one_add_α_pow_q, X.neg_fst, X.fst_intCast, X.one_snd, ω_pow_eq_neg_one, X.pow_ω, X.coe_mul, ω_pow_formula, X.zero_snd, X.snd_natCast
lucasLehmerResidue 📖	CompOp	1 math math: residue_eq_zero_iff_sMod_eq_zero
q 📖	CompOp	8 math math: mersenne_coe_X, ω_pow_eq_one, two_lt_q, ωUnit_coe, order_ω, ω_pow_eq_neg_one, ω_pow_formula, order_ineq
s 📖	CompOp	2 math math: X.closed_form, sZMod_eq_s
sMod 📖	CompOp	6 math math: sMod_lt, sMod_mod, sZMod_eq_sMod, residue_eq_zero_iff_sMod_eq_zero, sMod_nonneg, norm_num_ext.sModNat_eq_sMod
sZMod 📖	CompOp	2 math math: sZMod_eq_sMod, sZMod_eq_s
ωUnit 📖	CompOp	2 math math: ωUnit_coe, order_ω

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mersenne_coe_X 📖	mathematical	—	X PNat.val q X.instNatCast mersenne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing X.instCommRing	—	X.ext Nat.minFac_dvd
mersenne_int_ne_zero 📖	—	—	—	—	LT.lt.ne' mersenne_int_pos
mersenne_int_pos 📖	mathematical	—	Monoid.toNatPow Int.instMonoid	—	sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instAddLeftMono Nat.cast_one Int.instZeroLEOneClass Int.instCharZero
order_ineq 📖	mathematical	lucasLehmerResidue ZMod Monoid.toNatPow Nat.instMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	PNat.val q	—	NeZero.pnat order_ω orderOf_le_card_univ X.card_units_lt two_lt_q
order_ω 📖	mathematical	lucasLehmerResidue ZMod Monoid.toNatPow Nat.instMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	orderOf Units X PNat.val q X.instMonoid Units.instMonoid ωUnit	—	Nat.eq_prime_pow_of_dvd_least_prime_pow Nat.prime_two orderOf_dvd_iff_pow_eq_one ω_pow_eq_neg_one ZMod.neg_one_ne_one two_lt_q Units.ext ω_pow_eq_one
residue_eq_zero_iff_sMod_eq_zero 📖	mathematical	—	lucasLehmerResidue ZMod Monoid.toNatPow Nat.instMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing sMod	—	sZMod_eq_sMod Int.eq_zero_of_dvd_of_nonneg_of_lt Nat.instAtLeastTwoHAddOfNat sMod_nonneg ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat sMod_lt Nat.cast_pred LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass Nat.cast_pow Int.cast_zero
sMod_lt 📖	mathematical	—	sMod Monoid.toNatPow Int.instMonoid	—	sMod_mod LT.lt.trans_eq Int.emod_lt_abs mersenne_int_ne_zero abs_of_nonneg Int.instAddLeftMono LT.lt.le mersenne_int_pos
sMod_mod 📖	mathematical	—	sMod Monoid.toNatPow Int.instMonoid	—	—
sMod_nonneg 📖	mathematical	—	sMod	—	sup_eq_right mersenne_int_ne_zero
sZMod_eq_s 📖	mathematical	—	sZMod ZMod Monoid.toNatPow Nat.instMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing s	—	Nat.instAtLeastTwoHAddOfNat Int.cast_ofNat Int.cast_sub Int.cast_pow
sZMod_eq_sMod 📖	mathematical	—	sZMod ZMod Monoid.toNatPow Nat.instMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing sMod	—	Nat.instAtLeastTwoHAddOfNat Int.coe_nat_two_pow_pred ZMod.intCast_mod Int.cast_ofNat Int.cast_sub Int.cast_pow
two_lt_q 📖	mathematical	—	PNat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instOfNatPNatOfNeZeroNat q	—	LE.le.lt_of_ne' Nat.Prime.two_le Nat.minFac_prime LT.lt.ne' one_lt_mersenne Nat.minFac_eq_two_iff mersenne.eq_1 Nat.two_not_dvd_two_mul_sub_one
ωUnit_coe 📖	mathematical	—	Units.val X PNat.val q X.instMonoid ωUnit X.ω	—	—
ω_pow_eq_neg_one 📖	mathematical	lucasLehmerResidue ZMod Monoid.toNatPow Nat.instMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	X PNat.val q X.instMonoid X.ω NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid X.instAddCommGroup X.instOne	—	ω_pow_formula MulZeroClass.mul_zero MulZeroClass.zero_mul zero_sub mersenne_coe_X
ω_pow_eq_one 📖	mathematical	lucasLehmerResidue ZMod Monoid.toNatPow Nat.instMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	X PNat.val q X.instMonoid X.ω X.instOne	—	pow_mul ω_pow_eq_neg_one Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_pow
ω_pow_formula 📖	mathematical	lucasLehmerResidue ZMod Monoid.toNatPow Nat.instMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	X PNat.val q X.instMonoid X.ω SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup X.instAddGroupWithOne X.instMul AddGroupWithOne.toIntCast X.instNatCast mersenne X.instOne	—	Nat.instAtLeastTwoHAddOfNat add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.cast_pred LinearOrderedCommMonoidWithZero.toPosMulStrictMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.cast_pow sZMod_eq_s X.closed_form Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one eq_sub_of_add_eq mul_comm X.coe_mul one_pow X.ω_mul_ωb mul_pow pow_add mul_add Distrib.leftDistribClass Nat.cast_one Int.cast_natCast

LucasLehmer.X

Definitions

Name	Category	Theorems
instAddCommGroup 📖	CompOp	12 math math: two_mul_ω_pow, zero_fst, neg_snd, one_add_α_pow_q_succ, right_distrib, left_distrib, add_snd, add_fst, neg_fst, LucasLehmer.ω_pow_eq_neg_one, pow_ω, zero_snd
instAddGroupWithOne 📖	CompOp	8 math math: closed_form, coe_natCast, instCharP, snd_intCast, one_add_α_pow_q, fst_intCast, coe_mul, LucasLehmer.ω_pow_formula
instCoeZMod 📖	CompOp	—
instCommRing 📖	CompOp	6 math math: LucasLehmer.mersenne_coe_X, one_add_α_sq, one_add_α_pow_q_succ, closed_form, ω_pow_trace, one_add_α_pow_q
instDecidableEq 📖	CompOp	1 math math: card_units_lt
instFintype 📖	CompOp	2 math math: card_eq, card_units_lt
instInhabited 📖	CompOp	—
instMonoid 📖	CompOp	15 math math: two_mul_ω_pow, one_add_α_sq, one_add_α_pow_q_succ, α_pow, card_units_lt, LucasLehmer.ω_pow_eq_one, closed_form, ω_pow_trace, LucasLehmer.ωUnit_coe, LucasLehmer.order_ω, α_sq, one_add_α_pow_q, LucasLehmer.ω_pow_eq_neg_one, pow_ω, LucasLehmer.ω_pow_formula
instMul 📖	CompOp	11 math math: two_mul_ω_pow, one_add_α_sq, ωb_mul_ω, right_distrib, α_pow, left_distrib, mul_fst, ω_mul_ωb, mul_snd, coe_mul, LucasLehmer.ω_pow_formula
instNatCast 📖	CompOp	10 math math: fst_natCast, LucasLehmer.mersenne_coe_X, two_mul_ω_pow, one_add_α_sq, one_add_α_pow_q_succ, α_pow, coe_natCast, α_sq, LucasLehmer.ω_pow_formula, snd_natCast
instOne 📖	CompOp	11 math math: one_add_α_sq, one_add_α_pow_q_succ, ωb_mul_ω, LucasLehmer.ω_pow_eq_one, one_fst, ω_mul_ωb, one_add_α_pow_q, one_snd, LucasLehmer.ω_pow_eq_neg_one, pow_ω, LucasLehmer.ω_pow_formula
instRing 📖	CompOp	—
α 📖	CompOp	5 math math: one_add_α_sq, one_add_α_pow_q_succ, α_pow, α_sq, one_add_α_pow_q
ω 📖	CompOp	11 math math: two_mul_ω_pow, one_add_α_sq, ωb_mul_ω, LucasLehmer.ω_pow_eq_one, closed_form, ω_pow_trace, LucasLehmer.ωUnit_coe, ω_mul_ωb, LucasLehmer.ω_pow_eq_neg_one, pow_ω, LucasLehmer.ω_pow_formula
ωb 📖	CompOp	4 math math: ωb_mul_ω, closed_form, ω_pow_trace, ω_mul_ωb

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_fst 📖	mathematical	—	ZMod LucasLehmer.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	—
add_snd 📖	mathematical	—	ZMod LucasLehmer.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	—
card_eq 📖	mathematical	—	Fintype.card LucasLehmer.X instFintype Monoid.toNatPow Nat.instMonoid	—	Fintype.card_prod ZMod.card sq
card_units_lt 📖	mathematical	—	Fintype.card Units LucasLehmer.X instMonoid instFintypeUnitsOfDecidableEq instFintype instDecidableEq Monoid.toNatPow Nat.instMonoid	—	Fintype.card_congr' card_eq card_units_lt instNontrivialOfFactLtNatOfNat
closed_form 📖	mathematical	—	LucasLehmer.X AddGroupWithOne.toIntCast instAddGroupWithOne LucasLehmer.s Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Monoid.toNatPow instMonoid ω Nat.instMonoid ωb	—	ext Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_ofNat pow_one Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Nat.cast_one Mathlib.Meta.NormNum.isInt_neg Nat.cast_zero Nat.instAtLeastTwoHAddOfNat Int.cast_sub Int.cast_pow Int.cast_ofNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_congr mul_pow ωb_mul_ω one_pow mul_one add_sub_cancel_right pow_mul pow_succ
coe_mul 📖	mathematical	—	LucasLehmer.X AddGroupWithOne.toIntCast instAddGroupWithOne instMul	—	ext Int.cast_mul Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero add_zero MulZeroClass.zero_mul
coe_natCast 📖	mathematical	—	LucasLehmer.X AddGroupWithOne.toIntCast instAddGroupWithOne instNatCast	—	ext Int.cast_natCast
ext 📖	—	ZMod	—	—	—
ext_iff 📖	mathematical	—	ZMod	—	ext
fst_intCast 📖	mathematical	—	ZMod LucasLehmer.X AddGroupWithOne.toIntCast instAddGroupWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing	—	—
fst_natCast 📖	mathematical	—	ZMod LucasLehmer.X instNatCast AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing	—	—
instCharP 📖	mathematical	—	CharP LucasLehmer.X AddGroupWithOne.toAddMonoidWithOne instAddGroupWithOne	—	ext ZMod.natCast_eq_zero_iff
instNontrivialOfFactLtNatOfNat 📖	mathematical	—	Nontrivial LucasLehmer.X	—	zero_ne_one NeZero.one ZMod.nontrivial
left_distrib 📖	mathematical	—	LucasLehmer.X instMul AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup	—	ext Mathlib.Tactic.Ring.of_eq Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt
mul_fst 📖	mathematical	—	ZMod LucasLehmer.X instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	—
mul_snd 📖	mathematical	—	ZMod LucasLehmer.X instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing Distrib.toMul	—	—
neg_fst 📖	mathematical	—	ZMod LucasLehmer.X NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Ring.toAddCommGroup CommRing.toRing ZMod.commRing	—	—
neg_snd 📖	mathematical	—	ZMod LucasLehmer.X NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Ring.toAddCommGroup CommRing.toRing ZMod.commRing	—	—
ofNat_fst 📖	mathematical	—	ZMod instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing	—	—
ofNat_snd 📖	mathematical	—	ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	—
one_add_α_pow_q 📖	mathematical	Odd Nat.instSemiring legendreSym	LucasLehmer.X Monoid.toNatPow instMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing instOne α SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup instAddGroupWithOne	—	Nat.instAtLeastTwoHAddOfNat Int.cast_neg Int.cast_one Int.cast_ofNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial add_zero legendreSym.eq_pow add_pow_expChar expChar_prime instCharP α_pow dvd_rfl map_ofNat RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_neg RingHomClass.toAddMonoidHomClass one_pow ZMod.cast_one neg_mul one_mul sub_eq_add_neg
one_add_α_pow_q_succ 📖	mathematical	Odd Nat.instSemiring legendreSym	LucasLehmer.X Monoid.toNatPow instMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing instOne α NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat pow_succ one_add_α_pow_q mul_comm sq_sub_sq α_sq Mathlib.Meta.NormNum.isInt_eq_true Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isInt_neg
one_add_α_sq 📖	mathematical	—	LucasLehmer.X Monoid.toNatPow instMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing instOne α instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat ω	—	ext Nat.instAtLeastTwoHAddOfNat sq add_zero mul_one zero_add MulZeroClass.mul_zero Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_mul MulZeroClass.zero_mul
one_fst 📖	mathematical	—	ZMod LucasLehmer.X instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing	—	—
one_snd 📖	mathematical	—	ZMod LucasLehmer.X instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	—
pow_ω 📖	mathematical	Odd Nat.instSemiring legendreSym	LucasLehmer.X Monoid.toNatPow instMonoid ω NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup instOne	—	Nat.instAtLeastTwoHAddOfNat pow_succ legendreSym.eq_pow Int.cast_ofNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul two_mul_ω_pow dvd_rfl instCharP map_ofNat RingHom.instRingHomClass IsUnit.mul_left_cancel IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid Nat.cast_one Nat.cast_mul Even.two_dvd Odd.add_one Nat.cast_add CharP.cast_eq_zero zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass mul_pow
right_distrib 📖	mathematical	—	LucasLehmer.X instMul AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup	—	ext Mathlib.Tactic.Ring.of_eq Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt
snd_intCast 📖	mathematical	—	ZMod LucasLehmer.X AddGroupWithOne.toIntCast instAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	—
snd_natCast 📖	mathematical	—	ZMod LucasLehmer.X instNatCast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	—
two_mul_ω_pow 📖	mathematical	Odd Nat.instSemiring legendreSym	LucasLehmer.X Monoid.toNatPow instMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat ω NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat one_add_α_sq pow_mul even_iff_two_dvd Odd.add_one one_add_α_pow_q_succ
zero_fst 📖	mathematical	—	ZMod LucasLehmer.X NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	—
zero_snd 📖	mathematical	—	ZMod LucasLehmer.X NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	—
α_pow 📖	mathematical	—	LucasLehmer.X Monoid.toNatPow instMonoid α instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat pow_succ pow_mul α_sq
α_sq 📖	mathematical	—	LucasLehmer.X Monoid.toNatPow instMonoid α instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	ext Nat.instAtLeastTwoHAddOfNat sq MulZeroClass.mul_zero mul_one zero_add add_zero
ω_mul_ωb 📖	mathematical	—	LucasLehmer.X instMul ω ωb instOne	—	ext Nat.instAtLeastTwoHAddOfNat mul_one mul_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Nat.cast_one one_mul neg_add_cancel
ω_pow_trace 📖	mathematical	Odd Nat.instSemiring legendreSym	LucasLehmer.X Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Monoid.toNatPow instMonoid ω ωb MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	pow_ω Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.neg_mul mul_one one_pow ω_mul_ωb mul_pow mul_assoc pow_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
ωb_mul_ω 📖	mathematical	—	LucasLehmer.X instMul ωb ω instOne	—	mul_comm ω_mul_ωb

LucasLehmer.norm_num_ext

Definitions

Name	Category	Theorems
evalLucasLehmerTest 📖	CompOp	—
sModNat 📖	CompOp	3 math math: sModNat_eq_sMod, sModNat_aux_eq, sModNatTR_eq_sModNat
sModNatTR 📖	CompOp	1 math math: sModNatTR_eq_sModNat
sModNat_aux 📖	CompOp	1 math math: sModNat_aux_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNat_lucasLehmerTest 📖	—	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne LucasLehmer.LucasLehmerTest	—	—	—
isNat_not_lucasLehmerTest 📖	—	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne LucasLehmer.LucasLehmerTest	—	—	—
sModNatTR_eq_sModNat 📖	mathematical	—	sModNatTR sModNat	—	sModNat_aux_eq
sModNat_aux_eq 📖	mathematical	—	sModNat_aux sModNat	—	sModNat_aux.eq_2 sModNat.eq_2
sModNat_eq_sMod 📖	mathematical	—	sModNat Monoid.toNatPow Nat.instMonoid LucasLehmer.sMod	—	IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat sModNat.eq_1 LucasLehmer.sMod.eq_1 Nat.cast_sub Nat.cast_pow Nat.cast_one sModNat.eq_2 LucasLehmer.sMod.eq_2 Nat.cast_add add_sub_assoc sub_eq_add_neg add_assoc add_comm
testFalseHelper 📖	mathematical	sModNatTR Monoid.toNatPow Nat.instMonoid	LucasLehmer.LucasLehmerTest	—	LucasLehmer.LucasLehmerTest.eq_1 LucasLehmer.residue_eq_zero_iff_sMod_eq_zero sModNat_eq_sMod sModNatTR_eq_sModNat
testTrueHelper 📖	mathematical	sModNatTR Monoid.toNatPow Nat.instMonoid	LucasLehmer.LucasLehmerTest	—	LucasLehmer.LucasLehmerTest.eq_1 LucasLehmer.residue_eq_zero_iff_sMod_eq_zero sModNat_eq_sMod sModNatTR_eq_sModNat

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalMersenne 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mersenne_pos_of_pos 📖	mathematical	—	mersenne	—	mersenne_pos

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_mersenne 📖	—	Nat.Prime mersenne	—	—	Nat.prime_of_pow_sub_one_prime Nat.not_prime_one

(root)

Definitions

Name	Category	Theorems
mersenne 📖	CompOp	18 math math: lucas_lehmer_sufficiency, LucasLehmer.mersenne_coe_X, mersenne_mod_eight, Mathlib.Meta.Positivity.mersenne_pos_of_pos, mersenne_le_mersenne, mersenne_pos, mersenne_mod_three, strictMono_mersenne, one_lt_mersenne, mersenne_succ, mersenne_mod_four, succ_mersenne, legendreSym_mersenne_two, mersenne_lt_mersenne, mersenne_zero, LucasLehmer.ω_pow_formula, mersenne_odd, legendreSym_mersenne_three

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
legendreSym_mersenne_three 📖	mathematical	Odd Nat.instSemiring	legendreSym mersenne	—	Nat.fact_prime_three legendreSym.quadratic_reciprocity_three_mod_four Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_natMod Mathlib.Meta.NormNum.isNat_ofNat mersenne_mod_four legendreSym.mod Nat.cast_one mersenne_mod_three legendreSym.congr_simp legendreSym.at_one
legendreSym_mersenne_two 📖	mathematical	—	legendreSym mersenne	—	mersenne_mod_eight legendreSym.at_two ZMod.χ₈_nat_eq_if_mod_eight
lucas_lehmer_necessity 📖	mathematical	Nat.Prime mersenne	LucasLehmer.LucasLehmerTest	—	LucasLehmer.sZMod_eq_s LucasLehmer.X.fst_intCast LucasLehmer.X.closed_form add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid LucasLehmer.X.ω_pow_trace Nat.instCharZero Nat.instAtLeastTwoHAddOfNat legendreSym_mersenne_three Nat.Prime.odd_of_ne_two Nat.Prime.of_mersenne legendreSym_mersenne_two succ_mersenne pow_add mul_div_cancel_right₀ Nat.instMulDivCancelClass Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0
lucas_lehmer_sufficiency 📖	mathematical	LucasLehmer.LucasLehmerTest	Nat.Prime mersenne	—	Mathlib.Tactic.Contrapose.contrapose₁ LucasLehmer.order_ineq Nat.minFac_sq_le_self mersenne_pos lt_of_lt_of_le not_lt_of_ge
mersenne_le_mersenne 📖	mathematical	—	mersenne	—	StrictMono.le_iff_le strictMono_mersenne
mersenne_lt_mersenne 📖	mathematical	—	mersenne	—	StrictMono.lt_iff_lt strictMono_mersenne
mersenne_mod_eight 📖	mathematical	—	mersenne	—	Nat.le_induction mersenne_succ
mersenne_mod_four 📖	mathematical	—	mersenne	—	Nat.le_induction mersenne_succ
mersenne_mod_three 📖	mathematical	Odd Nat.instSemiring	mersenne	—	Nat.le_induction mersenne_succ
mersenne_odd 📖	mathematical	—	Odd Nat.instSemiring mersenne	—	Nat.Even.sub_odd Nat.instAtLeastTwoHAddOfNat one_le_pow₀ Nat.instZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing one_le_two IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Even.pow_of_ne_zero even_two odd_one
mersenne_pos 📖	mathematical	—	mersenne	—	mersenne_lt_mersenne
mersenne_succ 📖	mathematical	—	mersenne	—	two_pos Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
mersenne_zero 📖	mathematical	—	mersenne	—	—
modEq_mersenne 📖	mathematical	—	Nat.ModEq Monoid.toNatPow Nat.instMonoid	—	Nat.ModEq.add_right Nat.ModEq.mul_right Nat.modEq_sub pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass zero_lt_two IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid one_mul
one_lt_mersenne 📖	mathematical	—	mersenne	—	mersenne_lt_mersenne
strictMono_mersenne 📖	mathematical	—	StrictMono Nat.instPreorder mersenne	—	Nat.instAtLeastTwoHAddOfNat two_pos Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid pow_lt_pow_right₀ LinearOrderedCommMonoidWithZero.toPosMulStrictMono Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat
succ_mersenne 📖	mathematical	—	mersenne Monoid.toNatPow Nat.instMonoid	—	mersenne.eq_1 tsub_add_cancel_of_le StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub one_le_pow₀ Nat.instZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat Nat.instCharZero

---

← Back to Index