Commit 2022-03-05 00:00 8e1da4e6
View on Github →feat(ring_theory/adjoin/basic): if a set of elements of a subobject commute, its closure/adjoin is also commutative (#12231) We show that if a set of elements of a subobject commute, its closure/adjoin is also commutative The subobjects include (additive) submonoids, (additive) subgroups, subsemirings, subrings, and subalgebras.