Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-21 11:38 0eb5e2d1

View on Github →

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.

Estimated changes