Commit 2023-07-03 01:56 5cd26e52

feat: Compare card of subgroup to card of group (#5347) Includes new lemmas, one that shows that the cardinality of a subgroup is at most the cardinality of the ambient group, and others which shows that the cardinality of the top group is equal to that of the ambient group, and that in fact this is iff.