Commit 2025-10-06 18:32 2a770fb2
View on Github →feat(Algebra/Subgroup/Lattice): mem_biSup_of_directedOn (#29990)
Generalization of existing mem_iSup_of_directed
On the way to characterization of the torsion subgroup as the sup over all subgroups of roots of unity