Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-25 11:18 4abbe10d

View on Github →

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_smulinv_smul_smul
  • units.smul_inv_smulsmul_inv_smul
  • units.smul_perm_hom, mul_action.to_permmul_action.to_perm_hom
  • units.smul_permmul_action.to_perm
  • units.smul_left_cancelsmul_left_cancel
  • units.smul_eq_iff_eq_inv_smulsmul_eq_iff_eq_inv_smul
  • units.smul_eq_zerosmul_eq_zero_iff_eq (to avoid clashing with smul_eq_zero)
  • units.smul_ne_zerosmul_ne_zero_iff_ne
  • homeomorph.smul_of_unithomeomorph.smul (the latter already existed, and the former was a special case)
  • units.measurable_const_smul_iffmeasurable_const_smul_iff
  • units.ae_measurable_const_smul_iffae_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.

Estimated changes