Commit 2023-01-01 23:53 1a98d5b8

View on Github →

feat: port Data.Int.AbsoluteValue (#1289) Another quickie

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/AbsoluteValue.lean

added theorem AbsoluteValue.map_units_int

added theorem AbsoluteValue.map_units_int_cast

added theorem AbsoluteValue.map_units_int_smul

added def Int.natAbsHom