mathlib

8e1da4e6 - feat(ring_theory/adjoin/basic): if a set of elements of a subobject commute, its closure/adjoin is also commutative (#12231)

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. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>