Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-16 03:46 09fd631b

View on Github →

feat(data/zmod/basic): val_min_abs (#1548)

feat(data/zmod/basic): val_min_abs
Update basic.lean
docstring and fix zmodp versions

Estimated changes

Modified src/data/zmod/basic.lean

added theorem zmod.coe_val_min_abs

added theorem zmod.nat_abs_val_min_abs_le

added def zmod.val_min_abs

added theorem zmod.val_min_abs_eq_zero

added theorem zmod.val_min_abs_zero

added theorem zmodp.coe_val_min_abs

added theorem zmodp.nat_abs_val_min_abs_le

added def zmodp.val_min_abs

added theorem zmodp.val_min_abs_eq_zero

added theorem zmodp.val_min_abs_zero