Commit 2023-03-04 08:59 c7b500d6

View on Github →

feat: port Topology.Algebra.Ring.Basic (#2614)

Estimated changes

Modified Mathlib.lean

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

added theorem continuous_of_continuousAt_one₂

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

added def AbsoluteValue.comp

added def RingTopology.coinduced

added theorem RingTopology.coinduced_continuous

added theorem RingTopology.ext

added def RingTopology.toAddGroupTopology.orderEmbedding

added def RingTopology.toAddGroupTopology

added theorem RingTopology.toTopologicalSpace_injective

added structure RingTopology

added def Subring.commRingTopologicalClosure

added theorem Subring.isClosed_topologicalClosure

added theorem Subring.le_topologicalClosure

added def Subring.topologicalClosure

added theorem Subring.topologicalClosure_minimal

added def Subsemiring.commSemiringTopologicalClosure

added theorem Subsemiring.isClosed_topologicalClosure

added theorem Subsemiring.le_topologicalClosure

added def Subsemiring.topologicalClosure

added theorem Subsemiring.topologicalClosure_coe

added theorem Subsemiring.topologicalClosure_minimal

added theorem TopologicalRing.of_add_group_of_nhds_zero

added theorem TopologicalRing.of_nhds_zero

added theorem TopologicalSemiring.continuousNeg_of_mul

added theorem TopologicalSemiring.toTopologicalRing

added theorem mulLeft_continuous

added theorem mulRight_continuous