Commit 2026-02-26 23:01 34e58df8

View on Github →

feat: Subobject.topologicalClosure_mono (#35205) This was missing for most subobjects. We add it for all of them and tag it with gcongr.

Estimated changes

Modified Mathlib/Topology/Algebra/Algebra.lean

added theorem Subalgebra.topologicalClosure_mono

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem Subgroup.topologicalClosure_mono

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

added theorem Submonoid.topologicalClosure_mono

added theorem Subsemigroup.topologicalClosure_mono

Modified Mathlib/Topology/Algebra/NonUnitalAlgebra.lean

added theorem NonUnitalSubalgebra.topologicalClosure_mono

Modified Mathlib/Topology/Algebra/NonUnitalStarAlgebra.lean

added theorem NonUnitalStarSubalgebra.topologicalClosure_mono

Modified Mathlib/Topology/Algebra/Ring/Basic.lean

added theorem NonUnitalSubring.topologicalClosure_mono

added theorem NonUnitalSubsemiring.topologicalClosure_mono

added theorem Subring.topologicalClosure_mono

added theorem Subsemiring.topologicalClosure_mono

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean