Documentation Verification Report

Basic

📁 Source: Mathlib/Topology/Algebra/Ring/Basic.lean

Statistics

Metric	Count
Definitions `comp`, `IsTopologicalRing`, `IsTopologicalSemiring`, `nonUnitalCommRingTopologicalClosure`, `topologicalClosure`, `nonUnitalCommSemiringTopologicalClosure`, `topologicalClosure`, `RingTopology`, `coinduced`, `inhabited`, `instCompleteLattice`, `instCompleteSemilatticeInf`, `instPartialOrder`, `toAddGroupTopology`, `orderEmbedding`, `toTopologicalSpace`, `commRingTopologicalClosure`, `topologicalClosure`, `commSemiringTopologicalClosure`, `topologicalClosure`	20
Theorems `topologicalRing`, `topologicalSemiring`, `of_addGroup_of_nhds_zero`, `of_nhds_zero`, `toContinuousNeg`, `toIsTopologicalSemiring`, `to_topologicalAddGroup`, `continuousNeg_of_mul`, `toContinuousAdd`, `toContinuousMul`, `toIsTopologicalRing`, `instIsTopologicalRing`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `topologicalClosure_minimal`, `instIsTopologicalSemiring`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `topologicalClosure_coe`, `topologicalClosure_minimal`, `instIsTopologicalRing`, `instIsTopologicalSemiring`, `coinduced_continuous`, `ext`, `ext_iff`, `toIsTopologicalRing`, `toTopologicalSpace_injective`, `continuousSMul`, `instIsTopologicalRing`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `topologicalClosure_minimal`, `continuousSMul`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `topologicalClosure_coe`, `topologicalClosure_minimal`, `topologicalSemiring`, `instContinuousAddForallOfIsTopologicalSemiring`, `instContinuousAddMulOpposite`, `instContinuousMulAddOpposite`, `instContinuousNegMulOpposite`, `instIsTopologicalRingAddOpposite`, `instIsTopologicalRingMulOpposite`, `instIsTopologicalRingProd`, `instIsTopologicalRingULift`, `instIsTopologicalSemiringAddOpposite`, `instIsTopologicalSemiringMulOpposite`, `instIsTopologicalSemiringProd`, `instIsTopologicalSemiringULift`, `mulLeft_continuous`, `mulRight_continuous`	52
Total	72

AbsoluteValue

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	2 math math: `LiesOver.comp_eq'`, `LiesOver.comp_eq`

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`topologicalRing` 📖	mathematical	—	`IsTopologicalRing`	—	`topologicalSemiring` `IsTopologicalAddGroup.toContinuousNeg` `topologicalAddGroup_of_discreteTopology`
`topologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring`	—	`continuousAdd_of_discreteTopology` `continuousMul_of_discreteTopology`

IsTopologicalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_addGroup_of_nhds_zero` 📖	mathematical	`Filter.Tendsto` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`IsTopologicalRing`	—	`IsTopologicalAddGroup.toContinuousAdd` `continuous_of_continuousAt_zero₂` `nhds_prod_eq` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `IsTopologicalAddGroup.toContinuousNeg`
`of_nhds_zero` 📖	mathematical	`Filter.Tendsto` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `Filter.map`	`IsTopologicalRing`	—	`IsTopologicalAddGroup.of_comm_of_nhds_zero` `of_addGroup_of_nhds_zero`
`toContinuousNeg` 📖	mathematical	—	`ContinuousNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`toIsTopologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`to_topologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`IsTopologicalSemiring.toContinuousAdd` `toIsTopologicalSemiring` `toContinuousNeg`

IsTopologicalSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousNeg_of_mul` 📖	mathematical	—	`ContinuousNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NonAssocRing.toNonUnitalNonAssocRing`	—	`neg_mul` `one_mul` `Continuous.fun_mul` `continuous_const` `continuous_id`
`toContinuousAdd` 📖	mathematical	—	`ContinuousAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`toContinuousMul` 📖	mathematical	—	`ContinuousMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`toIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `NonAssocRing.toNonUnitalNonAssocRing`	—	`continuousNeg_of_mul` `toContinuousMul`

NonUnitalSubring

Definitions

Name	Category	Theorems
`nonUnitalCommRingTopologicalClosure` 📖	CompOp	—
`topologicalClosure` 📖	CompOp	3 math math: `topologicalClosure_minimal`, `isClosed_topologicalClosure`, `le_topologicalClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `toNonUnitalRing`	—	`Subsemigroup.instMulMemClass` `Subsemigroup.continuousMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `AddSubgroup.instIsTopologicalAddGroupSubtypeMem` `IsTopologicalRing.to_topologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `IsTopologicalAddGroup.toContinuousNeg`
`isClosed_topologicalClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `instSetLike` `topologicalClosure`	—	`isClosed_closure`
`le_topologicalClosure` 📖	mathematical	—	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`subset_closure`
`topologicalClosure_minimal` 📖	mathematical	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_minimal`

NonUnitalSubsemiring

Definitions

Name	Category	Theorems
`nonUnitalCommSemiringTopologicalClosure` 📖	CompOp	—
`topologicalClosure` 📖	CompOp	4 math math: `isClosed_topologicalClosure`, `le_topologicalClosure`, `topologicalClosure_minimal`, `topologicalClosure_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTopologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `instNonUnitalSubsemiringClass`	—	`Subsemigroup.instMulMemClass` `Subsemigroup.continuousMul` `IsTopologicalSemiring.toContinuousMul` `AddSubmonoid.continuousAdd` `IsTopologicalSemiring.toContinuousAdd` `instNonUnitalSubsemiringClass`
`isClosed_topologicalClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `instSetLike` `topologicalClosure`	—	`isClosed_closure`
`le_topologicalClosure` 📖	mathematical	—	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`subset_closure`
`topologicalClosure_coe` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `instSetLike` `topologicalClosure` `closure`	—	—
`topologicalClosure_minimal` 📖	mathematical	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_minimal`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTopologicalRing` 📖	mathematical	`IsTopologicalRing`	`topologicalSpace` `nonUnitalNonAssocRing`	—	`instIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `continuousNeg` `IsTopologicalRing.toContinuousNeg`
`instIsTopologicalSemiring` 📖	mathematical	`IsTopologicalSemiring`	`topologicalSpace` `nonUnitalNonAssocSemiring`	—	`instContinuousAddForallOfIsTopologicalSemiring` `continuousMul` `IsTopologicalSemiring.toContinuousMul`

RingTopology

Definitions

Name	Category	Theorems
`coinduced` 📖	CompOp	1 math math: `coinduced_continuous`
`inhabited` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	—
`instCompleteSemilatticeInf` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`toAddGroupTopology` 📖	CompOp	—
`toTopologicalSpace` 📖	CompOp	4 math math: `ext_iff`, `toIsTopologicalRing`, `coinduced_continuous`, `toTopologicalSpace_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coinduced_continuous` 📖	mathematical	—	`Continuous` `toTopologicalSpace` `coinduced`	—	`continuous_sInf_rng` `Set.forall_mem_image` `continuous_iff_coinduced_le`
`ext` 📖	—	`TopologicalSpace.IsOpen` `toTopologicalSpace`	—	—	`toTopologicalSpace_injective` `TopologicalSpace.ext`
`ext_iff` 📖	mathematical	—	`TopologicalSpace.IsOpen` `toTopologicalSpace`	—	`ext`
`toIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `toTopologicalSpace` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`toTopologicalSpace_injective` 📖	mathematical	—	`RingTopology` `TopologicalSpace` `toTopologicalSpace`	—	—

RingTopology.toAddGroupTopology

Definitions

Name	Category	Theorems
`orderEmbedding` 📖	CompOp	—

Subring

Definitions

Name	Category	Theorems
`commRingTopologicalClosure` 📖	CompOp	—
`topologicalClosure` 📖	CompOp	3 math math: `topologicalClosure_minimal`, `le_topologicalClosure`, `isClosed_topologicalClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousSMul` 📖	mathematical	—	`ContinuousSMul` `Subring` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulAction.toSemigroupAction` `instTopologicalSpaceSubtype`	—	`Subsemiring.continuousSMul`
`instIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `Subring` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing`	—	`Submonoid.continuousMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `AddSubgroup.instIsTopologicalAddGroupSubtypeMem` `IsTopologicalRing.to_topologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `IsTopologicalAddGroup.toContinuousNeg`
`isClosed_topologicalClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Subring` `instSetLike` `topologicalClosure`	—	`isClosed_closure`
`le_topologicalClosure` 📖	mathematical	—	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`subset_closure`
`topologicalClosure_minimal` 📖	mathematical	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_minimal`

Subsemiring

Definitions

Name	Category	Theorems
`commSemiringTopologicalClosure` 📖	CompOp	—
`topologicalClosure` 📖	CompOp	4 math math: `isClosed_topologicalClosure`, `topologicalClosure_minimal`, `topologicalClosure_coe`, `le_topologicalClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousSMul` 📖	mathematical	—	`ContinuousSMul` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike` `smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `instTopologicalSpaceSubtype`	—	`Submonoid.continuousSMul`
`isClosed_topologicalClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Subsemiring` `Semiring.toNonAssocSemiring` `instSetLike` `topologicalClosure`	—	`isClosed_closure`
`le_topologicalClosure` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`subset_closure`
`topologicalClosure_coe` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `Semiring.toNonAssocSemiring` `instSetLike` `topologicalClosure` `closure`	—	—
`topologicalClosure_minimal` 📖	mathematical	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_minimal`
`topologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toNonAssocSemiring`	—	`Submonoid.continuousMul` `IsTopologicalSemiring.toContinuousMul` `AddSubmonoid.continuousAdd` `IsTopologicalSemiring.toContinuousAdd`

(root)

Definitions

Name	Category	Theorems
`IsTopologicalRing` 📖	CompData	39 math math: `NonUnitalSubring.instIsTopologicalRing`, `IsTopologicalRing.of_nhds_zero`, `MvPowerSeries.WithPiTopology.instIsTopologicalRing`, `RingFilterBasis.isTopologicalRing`, `IsTopologicalSemiring.toIsTopologicalRing`, `instIsTopologicalRingULift`, `RingTopology.toIsTopologicalRing`, `IsModuleTopology.isTopologicalRing`, `IsTopologicalDivisionRing.toIsTopologicalRing`, `instIsTopologicalRingAddOpposite`, `UniformSpace.topologicalRing`, `NumberField.InfiniteAdeleRing.instIsTopologicalRing`, `TopCommRingCat.forgetToTopCatTopologicalRing`, `Valued.instIsTopologicalRing`, `NonarchimedeanRing.toIsTopologicalRing`, `instIsTopologicalRingReal`, `instIsTopologicalRingMulOpposite`, `IsDedekindDomain.FiniteAdeleRing.instIsTopologicalRing`, `IsStrictOrderedRing.topologicalRing`, `NonUnitalSeminormedRing.toIsTopologicalRing`, `instIsTopologicalRingLocalization`, `Subring.instIsTopologicalRing`, `IsValuativeTopology.instIsTopologicalRing`, `TopCommRingCat.isTopologicalRing`, `NonUnitalSubalgebra.instIsTopologicalRing`, `ContinuousMap.instIsTopologicalRingOfLocallyCompactSpace`, `NonUnitalStarSubalgebra.instIsTopologicalRing`, `TrivSqZeroExt.instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite`, `PowerSeries.WithPiTopology.instIsTopologicalRing`, `DiscreteTopology.topologicalRing`, `NumberField.AdeleRing.instIsTopologicalRing`, `Rat.instIsTopologicalRing`, `Matrix.topologicalRing`, `topologicalRing_quotient`, `instIsTopologicalRingProd`, `IsTopologicalRing.of_norm`, `WithIdealFilter.instIsTopologicalRing`, `IsTopologicalRing.of_addGroup_of_nhds_zero`, `UniformSpace.Completion.topologicalRing`
`IsTopologicalSemiring` 📖	CompData	20 math math: `instIsTopologicalSemiringProd`, `IsTopologicalRing.toIsTopologicalSemiring`, `NonUnitalStarSubalgebra.instIsTopologicalSemiring`, `topologicalSemiring_of_contMDiffRing`, `instIsTopologicalSemiringULift`, `StarSubalgebra.instIsTopologicalSemiringSubtypeMem`, `NNReal.instIsTopologicalSemiring`, `DiscreteTopology.topologicalSemiring`, `PowerSeries.WithPiTopology.instIsTopologicalSemiring`, `ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace`, `instIsTopologicalSemiringSubtypeMemSubalgebra`, `TrivSqZeroExt.topologicalSemiring`, `Subsemiring.topologicalSemiring`, `instIsTopologicalSemiringMatrix`, `instIsTopologicalSemiringAddOpposite`, `NonUnitalSubsemiring.instIsTopologicalSemiring`, `NonUnitalSubalgebra.instIsTopologicalSemiring`, `instIsTopologicalSemiringMulOpposite`, `MvPowerSeries.WithPiTopology.instIsTopologicalSemiring`, `NNRat.instIsTopologicalSemiring`
`RingTopology` 📖	CompData	1 math math: `RingTopology.toTopologicalSpace_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousAddForallOfIsTopologicalSemiring` 📖	mathematical	`IsTopologicalSemiring`	`ContinuousAdd` `Pi.topologicalSpace` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`Pi.continuousAdd` `IsTopologicalSemiring.toContinuousAdd`
`instContinuousAddMulOpposite` 📖	mathematical	—	`ContinuousAdd` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`continuousAdd_induced` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`instContinuousMulAddOpposite` 📖	mathematical	—	`ContinuousMul` `AddOpposite` `AddOpposite.instTopologicalSpaceAddOpposite` `AddOpposite.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`continuousMul_induced` `MulEquivClass.instMulHomClass` `MulEquiv.instMulEquivClass`
`instContinuousNegMulOpposite` 📖	mathematical	—	`ContinuousNeg` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	`Topology.IsInducing.continuousNeg` `Homeomorph.isInducing`
`instIsTopologicalRingAddOpposite` 📖	mathematical	—	`IsTopologicalRing` `AddOpposite` `AddOpposite.instTopologicalSpaceAddOpposite` `AddOpposite.instNonUnitalNonAssocRing`	—	`instIsTopologicalSemiringAddOpposite` `IsTopologicalRing.toIsTopologicalSemiring` `instContinuousNegAddOpposite` `IsTopologicalRing.toContinuousNeg`
`instIsTopologicalRingMulOpposite` 📖	mathematical	—	`IsTopologicalRing` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instNonUnitalNonAssocRing`	—	`instIsTopologicalSemiringMulOpposite` `IsTopologicalRing.toIsTopologicalSemiring` `instContinuousNegMulOpposite` `IsTopologicalRing.toContinuousNeg`
`instIsTopologicalRingProd` 📖	mathematical	—	`IsTopologicalRing` `instTopologicalSpaceProd` `Prod.instNonUnitalNonAssocRing`	—	`instIsTopologicalSemiringProd` `IsTopologicalRing.toIsTopologicalSemiring` `Prod.continuousNeg` `IsTopologicalRing.toContinuousNeg`
`instIsTopologicalRingULift` 📖	mathematical	—	`IsTopologicalRing` `ULift.topologicalSpace` `ULift.nonUnitalNonAssocRing`	—	`instContinuousAddULift` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instContinuousMulULift` `IsTopologicalSemiring.toContinuousMul` `instContinuousNegULift` `IsTopologicalRing.toContinuousNeg`
`instIsTopologicalSemiringAddOpposite` 📖	mathematical	—	`IsTopologicalSemiring` `AddOpposite` `AddOpposite.instTopologicalSpaceAddOpposite` `AddOpposite.instNonUnitalNonAssocSemiring`	—	`AddOpposite.instContinuousAdd` `IsTopologicalSemiring.toContinuousAdd` `instContinuousMulAddOpposite` `IsTopologicalSemiring.toContinuousMul`
`instIsTopologicalSemiringMulOpposite` 📖	mathematical	—	`IsTopologicalSemiring` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instNonUnitalNonAssocSemiring`	—	`instContinuousAddMulOpposite` `IsTopologicalSemiring.toContinuousAdd` `MulOpposite.instContinuousMul` `IsTopologicalSemiring.toContinuousMul`
`instIsTopologicalSemiringProd` 📖	mathematical	—	`IsTopologicalSemiring` `instTopologicalSpaceProd` `Prod.instNonUnitalNonAssocSemiring`	—	`Prod.continuousAdd` `IsTopologicalSemiring.toContinuousAdd` `Prod.continuousMul` `IsTopologicalSemiring.toContinuousMul`
`instIsTopologicalSemiringULift` 📖	mathematical	—	`IsTopologicalSemiring` `ULift.topologicalSpace` `ULift.nonUnitalNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`instContinuousAddULift` `IsTopologicalSemiring.toContinuousAdd` `instContinuousMulULift` `IsTopologicalSemiring.toContinuousMul`
`mulLeft_continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddMonoidHom.instFunLike` `AddMonoidHom.mulLeft`	—	`Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `continuous_const` `continuous_id`
`mulRight_continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddMonoidHom.instFunLike` `AddMonoidHom.mulRight`	—	`Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `continuous_id` `continuous_const`

---

← Back to Index