Commit 2022-02-16 11:53 75421198

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.