Theorems · Theorem · number theory
ZMod.coe_valMinAbs
∀ {n : ℕ} (x : ZMod n), ↑x.valMinAbs = x- Defined in
- Mathlib.Data.ZMod.ValMinAbs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- sub_zeroproof · cited by 938
- Int.cast_natCastproof · cited by 393
- ZMod.valproof · cited by 159
- Int.cast_subproof · cited by 78
- ZMod.natCast_zmod_valproof · cited by 29
- ZMod.valMinAbsstatement and proof · cited by 28
- ZMod.natCast_selfproof · cited by 15
- ZMod.valMinAbs_def_posproof · cited by 10
Cited by8
Results whose statement or proof uses this declaration.
- Nat.sq_add_sq_zmodEqproof · cited by 2
- ZMod.injective_valMinAbsproof · cited by 2
- ZMod.valMinAbs_specproof · cited by 1
- Nat.Prime.sum_four_squaresproof · cited by 1
- ZMod.eq_neg_of_valMinAbs_eq_neg_valMinAbsproof · cited by 1
- ZMod.valMinAbs_neg_of_ne_halfproof · cited by 1
- ZMod.nonsquare_of_jacobiSym_eq_neg_oneproof · cited by 0
- ZMod.natAbs_valMinAbs_add_leproof · cited by 0