Theorems · Definition · number theory
ZMod.val
{n : ℕ} → ZMod n → ℕval a is a natural number defined as:
- for a : ZMod 0 it is the absolute value of a
- for a : ZMod n with 0 < n it is the least natural number in the equivalence class
See ZMod.valMinAbs for a variant that takes values in the integers.
- Defined in
- Mathlib.Data.ZMod.Basic
- Cited by
- 159 results in Mathlib
- Foundations
- Depth 9 from the axioms, rests on 32 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ZModstatement and proof · cited by 1,024
Cited by168
Results whose statement or proof uses this declaration.
- ZMod.castproof · cited by 87
- ZMod.natCast_zmod_valstatement and proof · cited by 29
- ZMod.valMinAbsproof · cited by 28
- ZMod.natCast_valstatement · cited by 27
- ZMod.val_ltstatement and proof · cited by 20
- ZMod.val_natCaststatement and proof · cited by 18
- ZMod.card_units_eq_totientproof · cited by 15
- ZMod.val_zerostatement and proof · cited by 12
- PadicInt.nthHomproof · cited by 10
- ZMod.valMinAbs_def_posstatement and proof · cited by 10
- ZMod.intCast_zmod_castproof · cited by 10
- ZMod.coe_valMinAbsproof · cited by 8