Theorems · Theorem · number theory
ZMod.valMinAbs_natCast_of_le_half
∀ {n a : ℕ}, a ≤ n / 2 → (↑a).valMinAbs = ↑a- Defined in
- Mathlib.Data.ZMod.ValMinAbs
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ZModstatement · cited by 1,024
- LE.le.trans_ltproof · cited by 795
- ZMod.valproof · cited by 159
- ZMod.valMinAbsstatement · cited by 28
- ZMod.val_natCastproof · cited by 18
- ZMod.valMinAbs_def_posproof · cited by 10
- Nat.div_lt_self'proof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- ZMod.valMinAbs_natCast_eq_selfproof · cited by 0