Commit 2023-11-01 10:38 51dd9ef2

View on Github →

refactor(GroupTheory/GroupAction/Basic): re-organise, rename, and make some variables implicit (#7786)

Re-organise the namespace and section structure of GroupTheory/GroupAction/Basic.lean.
Remove the namespaces MulAction.Stabilizer and AddAction.Stabilizer, renaming MulAction.Stabilizer.submonoid to MulAction.stabilizerSubmonoid.
Make variables for the monoid/group/set implicit when an element or subset is used in the statement.

Estimated changes

Modified Mathlib/CategoryTheory/Action.lean

modified def CategoryTheory.ActionCategory.stabilizerIsoEnd

modified theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_apply

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

deleted def MulAction.Stabilizer.submonoid

modified theorem MulAction.fixed_eq_iInter_fixedBy

modified theorem MulAction.mem_fixedBy

modified theorem MulAction.mem_orbit

added theorem MulAction.mem_stabilizerSubmonoid_iff

modified theorem MulAction.mem_stabilizer_iff

deleted theorem MulAction.mem_stabilizer_submonoid_iff

added def MulAction.stabilizerSubmonoid

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

modified theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/GroupTheory/PGroup.lean

Modified Mathlib/GroupTheory/Sylow.lean