Commit 2025-06-18 17:15 b6f082c1
View on Github →feat(Algebra/Group/Subgroup/Lattice): Add closure_union_one and closure_diff_one (#26063)
This PR adds lemmas closure (s ∪ {1}) = closure s and closure (s \ {1}) = closure s.
feat(Algebra/Group/Subgroup/Lattice): Add closure_union_one and closure_diff_one (#26063)
This PR adds lemmas closure (s ∪ {1}) = closure s and closure (s \ {1}) = closure s.