Mathlib Map

Theorems · Definition · number theory

LucasLehmer.X

ℕ → Type

We construct the ring X q as ℤ/qℤ + √3 ℤ/qℤ.

Defined in
Mathlib.NumberTheory.LucasLehmer
Cited by
42 results in Mathlib
Foundations
Depth 9 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

LucasLehmer.X.ω · cited by 12X.ωLucasLehmer.X.ext · cited by 10X.extLucasLehmer.X.α · cited by 6X.αLucasLehmer.X.ωb · cited by 6X.ωbLucasLehmer.X.ω_mul_ωb · cited by 3X.ω_mul_ωbLucasLehmer.X.closed_form · cited by 2X.closed_formLucasLehmer.ωUnit · cited by 2LucasLehmer.ωUnitLucasLehmer.ω_pow_eq_neg_one · cited by 2LucasLehmer.ω_pow_eq_neg_…LucasLehmer.X.α_sq · cited by 2X.α_sqLucasLehmer.X.card_eq · cited by 1X.card_eqLucasLehmer.X.card_units_lt · cited by 1X.card_units_ltLucasLehmer.mersenne_coe_X · cited by 1LucasLehmer.mersenne_coe_XLucasLehmer.X.coe_mul · cited by 1X.coe_mulLucasLehmer.order_ω · cited by 1LucasLehmer.order_ωLucasLehmer.X.fst_intCast · cited by 1X.fst_intCastZMod · cited by 1024ZModLucasLehmer.XCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • ZModproof · cited by 1,024

Cited by46

Results whose statement or proof uses this declaration.