Commit 2023-10-30 03:57 41b0e9c7

View on Github →

refactor: generalize Abs lemmas from rings to groups (#7976) Four lemmas are moved from Algebra/Order/Monoid/Defs.lean to Algebra/Order/Group/Defs.lean and generalized Four lemmas are moved from Algebra/Order/Ring/Abs.lean to Algebra/Order/Group/Abs.lean and generalized Four lemmas are added in Algebra/Order/Monoid/Defs.lean. They're special cases of one_le_pow_iff, but I can't import the file without offending assert_not_exists.

Estimated changes

added theorem abs_cases
added theorem abs_eq_neg_self
added theorem abs_eq_self
added theorem inv_le_self_iff
added theorem inv_lt_self_iff
added theorem le_inv_self_iff
added theorem lt_inv_self_iff
added theorem mul_self_le_one_iff
added theorem mul_self_lt_one_iff
added theorem one_le_mul_self_iff
added theorem one_lt_mul_self_iff
deleted theorem abs_cases
deleted theorem abs_eq_neg_self
deleted theorem abs_eq_self
deleted theorem le_neg_self_iff
deleted theorem lt_neg_self_iff
deleted theorem neg_le_self_iff
deleted theorem neg_lt_self_iff