mathlib

7247a3cc - refactor(algebra/group/defs): `inv_one_class`, `neg_zero_class` (#16187)

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