Theorem Subgroup.closure_union_one

Modification history

2025-06-18 17:15
Mathlib/Algebra/Group/Subgroup/Lattice.lean
feat(Algebra/Group/Subgroup/Lattice): Add `closure_union_one` and `closure_diff_one` (#26063) …
Added Subgroup.closure_union_oneView on Github →