Commit 2022-12-10 13:41 825e257f

View on Github →

feat port: Algebra.Order.Ring.Abs (#929) 10b4e499f43088dd3bb7b5796184ad5216648ab1 Easy peasy

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Ring/Abs.lean

added def absHom

added theorem abs_cases

added theorem abs_dvd

added theorem abs_dvd_abs

added theorem abs_dvd_self

added theorem abs_eq_iff_mul_self_eq

added theorem abs_eq_neg_self

added theorem abs_eq_self

added theorem abs_le_iff_mul_self_le

added theorem abs_le_one_iff_mul_self_le_one

added theorem abs_lt_iff_mul_self_lt

added theorem abs_mul

added theorem abs_mul_abs_self

added theorem abs_mul_self

added theorem abs_one

added theorem abs_sub_sq

added theorem abs_two

added theorem dvd_abs

added theorem max_zero_add_max_neg_zero_eq_abs_self

added theorem self_dvd_abs