Mathlib Map

Theorems · Definition · number theory

ZMod.valMinAbs

{n : ℕ} → ZMod n → ℤ

Returns the integer in the same equivalence class as x that is closest to 0. The result will be in the interval (-n/2, n/2].

Defined in
Mathlib.Data.ZMod.ValMinAbs
Cited by
28 results in Mathlib
Foundations
Depth 20 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ZMod.valMinAbs_def_pos · cited by 10ZMod.valMinAbs_def_posZMod.coe_valMinAbs · cited by 8ZMod.coe_valMinAbsZMod.natAbs_valMinAbs_le · cited by 5ZMod.natAbs_valMinAbs_leZMod.valMinAbs_mem_Ioc · cited by 3ZMod.valMinAbs_mem_IocNat.sq_add_sq_zmodEq · cited by 2Nat.sq_add_sq_zmodEqZMod.natAbs_valMinAbs_neg · cited by 2ZMod.natAbs_valMinAbs_negZMod.injective_valMinAbs · cited by 2ZMod.injective_valMinAbsZMod.valMinAbs_inj · cited by 1ZMod.valMinAbs_injZMod.valMinAbs_mul_two_eq_iff · cited by 1ZMod.valMinAbs_mul_two_eq…ZMod.eq_neg_of_valMinAbs_eq_neg_valMinAbs · cited by 1ZMod.eq_neg_of_valMinAbs_…ZMod.valMinAbs_natCast_of_le_half · cited by 1ZMod.valMinAbs_natCast_of…ZMod.natAbs_valMinAbs_eq_natAbs_valMinAbs · cited by 1ZMod.natAbs_valMinAbs_eq_…ZMod.valMinAbs_neg_of_ne_half · cited by 1ZMod.valMinAbs_neg_of_ne_…ZMod.valMinAbs_nonneg_iff · cited by 1ZMod.valMinAbs_nonneg_iffZMod.valMinAbs_spec · cited by 1ZMod.valMinAbs_specZMod · cited by 1024ZModZMod.val · cited by 159ZMod.valZMod.valMinAbsCITED BYCITES

Cites2

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.valproof · cited by 159

Cited by28

Results whose statement or proof uses this declaration.