Commit 2024-10-17 15:03 d0df6356
View on Github →feat(QuotientGroup,Ideal/Quotient): group is finite if quotient is finite (#15425) Does not actually require the subgroup to be normal Also provides a breakdown of the group as the disjoint indexed union of cosets