mathlib

75421198 - refactor(algebra/group/basic): add extra typeclasses for negation (#11960)

refactor(algebra/group/basic): add extra typeclasses for negation (#11960) The new typeclasses are: * `has_involutive_inv R`, stating that `(r⁻¹)⁻¹ = r` (instances: `group`, `group_with_zero`, `ennreal`, `set`, `submonoid`) * `has_involutive_neg R`, stating that `- -r = r` (instances: `add_group`, `ereal`, `module.ray`, `ray_vector`, `set`, `add_submonoid`, `jordan_decomposition`) * `has_distrib_neg R`, stating that `-a * b = a * -b = -(a * b)` (instances: `ring`, `units`, `unitary`, `special_linear_group`, `GL_pos`) While the original motivation only concerned the two `neg` typeclasses, the `to_additive` machinery forced the introduction of `has_involutive_inv`, which turned out to be used in more places than expected. Adding these typeclases removes a large number of specialized `units R` lemmas as the lemmas about `R` now match themselves. A surprising number of lemmas elsewhere in the library can also be removed. The removed lemmas are: * Lemmas about `units` (replaced by `units.has_distrib_neg`): * `units.neg_one_pow_eq_or` * `units.neg_pow` * `units.neg_pow_bit0` * `units.neg_pow_bit1` * `units.neg_sq` * `units.neg_inv` (now `inv_neg'` for arbitrary groups with distributive negation) * `units.neg_neg` * `units.neg_mul` * `units.mul_neg` * `units.neg_mul_eq_neg_mul` * `units.neg_mul_eq_mul_neg` * `units.neg_mul_neg` * `units.neg_eq_neg_one_mul` * `units.mul_neg_one` * `units.neg_one_mul` * `semiconj_by.units_neg_right` * `semiconj_by.units_neg_right_iff` * `semiconj_by.units_neg_left` * `semiconj_by.units_neg_left_iff` * `semiconj_by.units_neg_one_right` * `semiconj_by.units_neg_one_left` * `commute.units_neg_right` * `commute.units_neg_right_iff` * `commute.units_neg_left` * `commute.units_neg_left_iff` * `commute.units_neg_one_right` * `commute.units_neg_one_left` * Lemmas about groups with zero (replaced by `group_with_zero.to_has_involutive_neg`): * `inv_inv₀` * `inv_involutive₀` * `inv_injective₀` * `inv_eq_iff` (now shared with the `inv_eq_iff_inv_eq` group lemma) * `eq_inv_iff` (now shared with the `eq_inv_iff_eq_inv` group lemma) * `equiv.inv₀` * `measurable_equiv.inv₀` * Lemmas about `ereal` (replaced by `ereal.has_involutive_neg`): * `ereal.neg_neg` * `ereal.neg_inj` * `ereal.neg_eq_neg_iff` * `ereal.neg_eq_iff_neg_eq` * Lemmas about `ennreal` (replaced by `ennreal.has_involutive_inv`): * `ereal.inv_inv` * `ereal.inv_involutive` * `ereal.inv_bijective` * `ereal.inv_eq_inv` * Other lemmas: * `ray_vector.neg_neg` * `module.ray.neg_neg` * `module.ray.neg_involutive` * `module.ray.eq_neg_iff_eq_neg` * `set.inv_inv` * `set.neg_neg` * `submonoid.inv_inv` * `add_submonoid.neg_neg` As a bonus, this provides the group `unitary R` with a negation operator and all the lemmas listed for `units` above. For now this doesn't attempt to unify `units.neg_smul` and `neg_smul`.