Mathlib Map

Theorems · Theorem · number theory

ZMod.valMinAbs_def_pos

∀ {n : ℕ} [NeZero n] (x : ZMod n), x.valMinAbs = if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n
Defined in
Mathlib.Data.ZMod.ValMinAbs
Cited by
10 results in Mathlib
Foundations
Depth 21 from the axioms · uses propext
Assumes
NeZero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ZMod.coe_valMinAbs · cited by 8ZMod.coe_valMinAbsZMod.valMinAbs_mem_Ioc · cited by 3ZMod.valMinAbs_mem_IocZMod.valMinAbs_zero · cited by 1ZMod.valMinAbs_zeroZMod.natCast_natAbs_valMinAbs · cited by 1ZMod.natCast_natAbs_valMi…ZMod.valMinAbs_natCast_of_le_half · cited by 1ZMod.valMinAbs_natCast_of…ZMod.valMinAbs_nonneg_iff · cited by 1ZMod.valMinAbs_nonneg_iffZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id · cited by 0ZMod.Ico_map_valMinAbs_na…ZMod.val_eq_ite_valMinAbs · cited by 0ZMod.val_eq_ite_valMinAbsZMod.valMinAbs_natAbs_eq_min · cited by 0ZMod.valMinAbs_natAbs_eq_…ZMod.valMinAbs_natCast_of_half_lt · cited by 0ZMod.valMinAbs_natCast_of…ZMod · cited by 1024ZModZMod.val · cited by 159ZMod.valZMod.valMinAbs · cited by 28ZMod.valMinAbsZMod.valMinAbs_def_posCITED BYCITES

Cites3

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
  • ZMod.valstatement and proof · cited by 159
  • ZMod.valMinAbsstatement and proof · cited by 28

Cited by10

Results whose statement or proof uses this declaration.