Commit 2021-05-25 11:18 4abbe10d

feat(group_theory/group_action/units): group actions on and by units (#7438) This removes all the lemmas about (u : α) • x and (↑u⁻¹ : α) • x in favor of granting units α its very own has_scalar structure, along with providing the stronger variants to make it usable elsewhere. This means that downstream code need only reason about [group G] [mul_action G M] instead of needing to handle groups and units separately. The (multiplicative versions of the) removed and moved lemmas are:

• units.inv_smul_smul → inv_smul_smul
• units.smul_inv_smul → smul_inv_smul
• units.smul_perm_hom, mul_action.to_perm → mul_action.to_perm_hom
• units.smul_perm → mul_action.to_perm
• units.smul_left_cancel → smul_left_cancel
• units.smul_eq_iff_eq_inv_smul → smul_eq_iff_eq_inv_smul
• units.smul_eq_zero → smul_eq_zero_iff_eq (to avoid clashing with smul_eq_zero)
• units.smul_ne_zero → smul_ne_zero_iff_ne
• homeomorph.smul_of_unit → homeomorph.smul (the latter already existed, and the former was a special case)
• units.measurable_const_smul_iff → measurable_const_smul_iff
• units.ae_measurable_const_smul_iff → ae_measurable_const_smul_iff The new lemmas are:
• smul_eq_zero_iff_eq', a group_with_zero version of smul_eq_zero_iff_eq
• smul_ne_zero_iff_ne', a group_with_zero version of smul_ne_zero_iff_ne
• units.neg_smul, a version of neg_smul for units. We don't currently have typeclasses about neg on objects without +. We also end up needing some new typeclass instances downstream
• units.measurable_space
• units.has_measurable_smul
• units.has_continuous_smul This goes on to remove lots of coercions from alternating_map, matrix.det, and some lie algebra stuff. This makes the theorem statement cleaner, but occasionally requires rewriting through units.smul_def to add or remove the coercion.