Commit 2023-01-20 23:55 6f9f3636
View on Github →chore(group_theory/subgroup/basic): split out finiteness (#18242) It feels like it should be possible to define subgroups without relying on all the infrastructure about finite sets and types, and it turns out that it is with fairly limited work. This also has the advantage of removing a few hundred lines of code from what's still one of mathlib's biggest files.