Commit 2023-07-24 08:57 4be58905View on Github →
subgroup G to
set G (#18965)
This is consistent with all the other
This generalization reveals that a lot of downstream results are rather strangely stated about
This does not attempt to change these, instead leaving the work for a follow up (either in a later mathlib3 PR or in mathlib4).