Theorems · Definition · number theory
ZMod
ℕ → Type
The integers modulo n : ℕ.
- Defined in
- Mathlib.Data.ZMod.Defs
- Cited by
- 1,024 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 26 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by1,181
Results whose statement or proof uses this declaration.
- DirichletCharacterproof · cited by 161
- ZMod.valstatement and proof · cited by 159
- ZMod.caststatement and proof · cited by 87
- ZMod.castHomstatement · cited by 55
- legendreSymproof · cited by 51
- LucasLehmer.Xproof · cited by 42
- ZMod.cardstatement and proof · cited by 36
- CliffordAlgebra.evenOddstatement and proof · cited by 35
- ZMod.toAddCirclestatement · cited by 32
- CongruenceSubgroup.Gammaproof · cited by 31
- ZMod.natCast_zmod_valstatement and proof · cited by 29
- DirichletCharacter.changeLevelstatement · cited by 29
Showing the 200 most cited of 1,181.