Commit 2023-08-11 20:30 ad9a95ec

View on Github →

refactor(GroupTheory/GroupAction/Basic): rename variable names to a consistent style (#6531) Renaming variable names in basic definitions, theorems, and proofs regarding MulAction and AddAction, so that the choice of letter is

  1. consistent with sibling files (e.g. GroupTheory/GroupAction/Defs.lean) and
  2. easy to parse. Specifically,
  • M (for "monoid") or G (for "group") is the type that acts;
  • α is the type that is acted on;
  • terms of M are m etc and terms of G are g etc;
  • terms of α are a etc. Miswording in the docstrings for MulAction.fixedBy and AddAction.fixedby is also fixed.

Estimated changes

modified def MulAction.fixedBy
modified def MulAction.fixedPoints
modified theorem MulAction.mapsTo_smul_orbit
modified theorem MulAction.mem_fixedBy
modified theorem MulAction.mem_fixedPoints'
modified theorem MulAction.mem_fixedPoints
modified theorem MulAction.mem_orbit
modified theorem MulAction.mem_orbit_iff
modified theorem MulAction.mem_orbit_self
modified theorem MulAction.mem_orbit_smul
modified theorem MulAction.orbit.coe_smul
modified def MulAction.orbit
modified def MulAction.orbitRel
modified theorem MulAction.orbitRel_apply
modified theorem MulAction.orbit_eq_iff
modified theorem MulAction.orbit_eq_univ
modified theorem MulAction.orbit_nonempty
modified theorem MulAction.orbit_smul
modified theorem MulAction.orbit_smul_subset
modified theorem MulAction.smul_orbit
modified theorem MulAction.smul_orbit_subset
modified def MulAction.stabilizer