Theorem ZMod.natCast_natAbs_valMinAbs

Modification history

2025-02-01 07:23
Mathlib/Data/ZMod/Basic.lean
chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308)
Modified ZMod.natCast_natAbs_valMinAbsView on Github →
2024-04-17 11:15
Mathlib/Data/ZMod/Basic.lean
chore: Rename `nat_cast`/`int_cast`/`rat_cast` to `natCast`/`intCast`/`ratCast` (#11486) …
Added ZMod.natCast_natAbs_valMinAbsView on Github →