Commit 2025-10-22 17:48 40d354e1

View on Github →

feat(ValMinAbs): add lemmas (#28837)

Estimated changes

Modified Mathlib/Data/ZMod/ValMinAbs.lean

added theorem ZMod.abs_valMinAbs_eq_abs_valMinAbs

added theorem ZMod.eq_neg_of_valMinAbs_eq_neg_valMinAbs

added theorem ZMod.natAbs_valMinAbs_eq_natAbs_valMinAbs

modified theorem ZMod.valMinAbs_eq_zero

added theorem ZMod.valMinAbs_inj