Commit 2024-06-04 21:42 96d2f1fa

View on Github →

chore: Scope some extremely generic notation (#13518) In addition this notation was used exactly twice in Mathlib…

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

modified theorem FixedPoints.mem_subgroup

modified def FixedPoints.subgroup

modified theorem FixedPoints.subgroup_toSubmonoid