Commit 2025-11-14 17:31 ae79ea3a
View on Github →feat: Subgroup.mem_sup for arbitrary groups when one of the subgroups is normal (#31458) We prove Subgroup.mem_sup for arbitrary (not necessarily commutative) groups when one of the subgroups is normal.