Commit 2022-12-14 08:49 1fece095

View on Github →

feat: port Algebra.Order.AbsoluteValue (#974) mathlib SHA: fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/AbsoluteValue.lean

added theorem AbsoluteValue.abs_abv_sub_le_abv_sub

added theorem AbsoluteValue.coe_mk

added theorem AbsoluteValue.coe_toMonoidWithZeroHom

added theorem AbsoluteValue.coe_toMulHom

added theorem AbsoluteValue.coe_to_monoid_hom

added theorem AbsoluteValue.ext

added theorem AbsoluteValue.map_one_of_is_regular

added theorem AbsoluteValue.map_sub_eq_zero_iff

added def AbsoluteValue.toMonoidHom

added def AbsoluteValue.toMonoidWithZeroHom

added structure AbsoluteValue

added theorem IsAbsoluteValue.abs_abv_sub_le_abv_sub

added def IsAbsoluteValue.abvHom'

added def IsAbsoluteValue.abvHom

added theorem IsAbsoluteValue.abv_div

added theorem IsAbsoluteValue.abv_inv

added theorem IsAbsoluteValue.abv_neg

added theorem IsAbsoluteValue.abv_one'

added theorem IsAbsoluteValue.abv_one

added theorem IsAbsoluteValue.abv_pos

added theorem IsAbsoluteValue.abv_pow

added theorem IsAbsoluteValue.abv_sub

added theorem IsAbsoluteValue.abv_sub_le

added theorem IsAbsoluteValue.abv_zero

added theorem IsAbsoluteValue.sub_abv_le_abv_sub

added def IsAbsoluteValue.toAbsoluteValue