Commit 2024-11-11 23:00 69fd8707

View on Github →

feat: topological closure of non-unital subobjects (#18613) This adds *.topologicalClosure and the related fundamental lemmas for each of Semigroup, AddSemigroup, NonUnitalSemiring, NonUnitalSubring, NonUnitalAlgebra and NonUnitalStarAlgebra, thereby filling a gap in our API for these objects.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

added theorem MulHom.isClosed_range_coe

added theorem Subsemigroup.coe_topologicalClosure

added theorem Subsemigroup.isClosed_topologicalClosure

added theorem Subsemigroup.le_topologicalClosure

added theorem Subsemigroup.top_closure_mul_self_subset

added def Subsemigroup.topologicalClosure

added theorem Subsemigroup.topologicalClosure_minimal

added def mulHomOfMemClosureRangeCoe

added def mulHomOfTendsto

Created Mathlib/Topology/Algebra/NonUnitalAlgebra.lean

added theorem NonUnitalSubalgebra.isClosed_topologicalClosure

added theorem NonUnitalSubalgebra.le_topologicalClosure

added def NonUnitalSubalgebra.topologicalClosure

added theorem NonUnitalSubalgebra.topologicalClosure_minimal

Created Mathlib/Topology/Algebra/NonUnitalStarAlgebra.lean

added theorem NonUnitalStarSubalgebra.isClosed_topologicalClosure

added theorem NonUnitalStarSubalgebra.le_topologicalClosure

added def NonUnitalStarSubalgebra.topologicalClosure

added theorem NonUnitalStarSubalgebra.topologicalClosure_minimal

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

added theorem NonUnitalSubring.isClosed_topologicalClosure

added theorem NonUnitalSubring.le_topologicalClosure

added def NonUnitalSubring.topologicalClosure

added theorem NonUnitalSubring.topologicalClosure_minimal

added theorem NonUnitalSubsemiring.isClosed_topologicalClosure

added theorem NonUnitalSubsemiring.le_topologicalClosure

added def NonUnitalSubsemiring.topologicalClosure

added theorem NonUnitalSubsemiring.topologicalClosure_coe

added theorem NonUnitalSubsemiring.topologicalClosure_minimal