Commit 2023-04-07 10:08 e39b2102

View on Github →

feat: port Topology.Algebra.StarSubalgebra (#3319)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/StarSubalgebra.lean

added theorem StarAlgHom.ext_topologicalClosure

added theorem StarAlgHomClass.ext_topologicalClosure

added theorem StarSubalgebra.closedEmbedding_inclusion

added def StarSubalgebra.commRingTopologicalClosure

added def StarSubalgebra.commSemiringTopologicalClosure

added theorem StarSubalgebra.embedding_inclusion

added theorem StarSubalgebra.isClosed_topologicalClosure

added theorem StarSubalgebra.le_topologicalClosure

added def StarSubalgebra.topologicalClosure

added theorem StarSubalgebra.topologicalClosure_coe

added theorem StarSubalgebra.topologicalClosure_minimal

added theorem StarSubalgebra.topologicalClosure_mono

added theorem elementalStarAlgebra.closedEmbedding_coe

added theorem elementalStarAlgebra.le_of_isClosed_of_mem

added theorem elementalStarAlgebra.self_mem

added theorem elementalStarAlgebra.starAlgHomClass_ext

added theorem elementalStarAlgebra.star_self_mem

added def elementalStarAlgebra