Theorems · Theorem · number theory
LucasLehmer.mersenne_coe_X
∀ (p : ℕ), ↑(mersenne p) = 0
q is the minimum factor of mersenne p, so M p = 0 in X q.
- Defined in
- Mathlib.NumberTheory.LucasLehmer
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PNat.valstatement · cited by 226
- Nat.minFacproof · cited by 72
- LucasLehmer.Xstatement · cited by 42
- mersennestatement · cited by 22
- LucasLehmer.X.extproof · cited by 10
- LucasLehmer.qstatement · cited by 9
Cited by1
Results whose statement or proof uses this declaration.
- LucasLehmer.ω_pow_eq_neg_oneproof · cited by 2