Commit 2023-04-05 08:46 9a8d2c4f

View on Github →

feat: port Topology.Algebra.Algebra (#3271)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Algebra.lean

added def Algebra.elementalAlgebra

added theorem Algebra.self_mem_elementalAlgebra

added def Subalgebra.commRingTopologicalClosure

added def Subalgebra.commSemiringTopologicalClosure

added theorem Subalgebra.isClosed_topologicalClosure

added theorem Subalgebra.le_topologicalClosure

added def Subalgebra.topologicalClosure

added theorem Subalgebra.topologicalClosure_coe

added theorem Subalgebra.topologicalClosure_comap_homeomorph

added theorem Subalgebra.topologicalClosure_minimal

added def algebraMapClm

added theorem algebraMapClm_coe

added theorem algebraMapClm_toLinearMap

added theorem continuousSMul_of_algebraMap

added theorem continuous_algebraMap

added theorem continuous_algebraMap_iff_smul

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