Commit 2022-09-28 15:55 7247a3cc

refactor(algebra/group/defs): inv_one_class, neg_zero_class (#16187) Define typeclasses inv_one_class and neg_zero_class, to allow results depending on those properties to be proved more generally than for division_monoid and subtraction_monoid without requiring duplication. Also define div_inv_one_monoid and sub_neg_zero_monoid. The only instances added here are those deduced from division_monoid and subtraction_monoid, and the only lemmas generalized to these classes were previously proved for those classes. Additional instances intended for followups include:

• neg_zero_class for the combination of mul_zero_class with has_distrib_neg, so eliminating the separate neg_zero' lemma.
• sub_neg_zero_monoid for ereal.
• div_inv_one_monoid for ennreal.
• The usual pointwise, pi and prod instances. Additional lemmas intended to be generalized to use these typeclasses in followups include:
• antiperiodic.nat_mul_eq_of_eq_zero and antiperiodic.int_mul_eq_of_eq_zero, which currently require the codomain of the antiperiodic function to be a subtraction_monoid. (The latter will also require involutive neg, as will some lemmas about inequalities.)
• Given appropriate typeclasses for the interaction of inequalities with inv and neg (which will also enabling combining left and right variants, which is the main motivation of these changes), lemmas such as left.inv_le_one_iff, left.one_le_inv_iff, left.one_lt_inv_iff, left.inv_lt_one_iff and their right and additive variants. Some of these currently have duplicates for ennreal, for example. Zulip thread raising question of such typeclasses: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/typeclasses.20for.20orders.20with.20neg.20and.20inv