mathlib

0eb5e2d1 - feat(topology/algebra): if a subobject is commutative, then so is its topological closure (#12170)

feat(topology/algebra): if a subobject is commutative, then so is its topological closure (#12170) We prove that if a submonoid (or subgroup, subsemiring, subring, subalgebra, and the additive versions where applicable) is commutative, then so is its topological closure.