Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-16 18:58 1b098c06

View on Github →

feat(algebra/ordered_group, algebra/ordered_ring): add some lemmas about abs (#7612)

Estimated changes

added theorem abs_choice
added theorem abs_eq_abs
added theorem eq_or_eq_neg_of_abs_eq
added theorem abs_dvd
added theorem abs_dvd_abs
added theorem abs_dvd_self
added theorem dvd_abs
added theorem even_abs
added theorem self_dvd_abs