Basic

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

Statistics

Metric	Count
Definitions `comp`, `IsSemitopologicalRing`, `IsSemitopologicalSemiring`, `IsTopologicalRing`, `IsTopologicalSemiring`, `nonUnitalCommRingTopologicalClosure`, `topologicalClosure`, `nonUnitalCommSemiringTopologicalClosure`, `topologicalClosure`, `RingTopology`, `coinduced`, `inhabited`, `instCompleteLattice`, `instCompleteSemilatticeInf`, `instPartialOrder`, `toAddGroupTopology`, `orderEmbedding`, `toTopologicalSpace`, `commRingTopologicalClosure`, `topologicalClosure`, `commSemiringTopologicalClosure`, `topologicalClosure`	22
Theorems `topologicalRing`, `topologicalSemiring`, `toContinuousNeg`, `toIsSemitopologicalSemiring`, `toIsTopologicalAddGroup`, `continuousNeg_of_mul`, `toContinuousAdd`, `toIsSemitopologicalRing`, `toSeparatelyContinuousMul`, `of_addGroup_of_nhds_zero`, `of_nhds_zero`, `toContinuousNeg`, `toIsSemitopologicalRing`, `toIsTopologicalSemiring`, `to_topologicalAddGroup`, `continuousNeg_of_mul`, `toContinuousAdd`, `toContinuousMul`, `toIsSemitopologicalSemiring`, `toIsTopologicalRing`, `instIsSemitopologicalRing`, `instIsTopologicalRing`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `topologicalClosure_minimal`, `topologicalClosure_mono`, `instIsSemitopologicalSemiring`, `instIsTopologicalSemiring`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `topologicalClosure_coe`, `topologicalClosure_minimal`, `topologicalClosure_mono`, `instIsSemitopologicalRing`, `instIsSemitopologicalSemiring`, `instIsTopologicalRing`, `instIsTopologicalSemiring`, `coinduced_continuous`, `ext`, `ext_iff`, `toIsTopologicalRing`, `toTopologicalSpace_injective`, `continuousSMul`, `instIsSemitopologicalRing`, `instIsTopologicalRing`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `topologicalClosure_minimal`, `topologicalClosure_mono`, `continuousSMul`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `semitopologicalSemiring`, `topologicalClosure_coe`, `topologicalClosure_minimal`, `topologicalClosure_mono`, `topologicalSemiring`, `instContinuousAddMulOpposite`, `instContinuousMulAddOpposite`, `instContinuousNegMulOpposite`, `instIsSemitopologicalRingAddOpposite`, `instIsSemitopologicalRingMulOpposite`, `instIsSemitopologicalRingProd`, `instIsSemitopologicalSemiringAddOpposite`, `instIsSemitopologicalSemiringMulOpposite`, `instIsSemitopologicalSemiringProd`, `instIsTopologicalRingAddOpposite`, `instIsTopologicalRingMulOpposite`, `instIsTopologicalRingProd`, `instIsTopologicalRingULift`, `instIsTopologicalSemiringAddOpposite`, `instIsTopologicalSemiringMulOpposite`, `instIsTopologicalSemiringProd`, `instIsTopologicalSemiringULift`, `instSeparatelyContinuousMulAddOpposite`, `mulLeft_continuous`, `mulRight_continuous`	77
Total	99

AbsoluteValue

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	2 math math: `NumberField.InfinitePlace.coe_mk_comp`, `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`

IsSemitopologicalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContinuousNeg` 📖	mathematical	—	`ContinuousNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`toIsSemitopologicalSemiring` 📖	mathematical	—	`IsSemitopologicalSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`toIsTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`IsSemitopologicalSemiring.toContinuousAdd` `toIsSemitopologicalSemiring` `toContinuousNeg`

IsSemitopologicalSemiring

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.const_mul` `continuous_id`
`toContinuousAdd` 📖	mathematical	—	`ContinuousAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`toIsSemitopologicalRing` 📖	mathematical	—	`IsSemitopologicalRing` `NonAssocRing.toNonUnitalNonAssocRing`	—	`continuousNeg_of_mul` `toSeparatelyContinuousMul`
`toSeparatelyContinuousMul` 📖	mathematical	—	`SeparatelyContinuousMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—

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`	—	—
`toIsSemitopologicalRing` 📖	mathematical	—	`IsSemitopologicalRing`	—	`IsTopologicalSemiring.toContinuousAdd` `toIsTopologicalSemiring` `instSeparatelyContinuousMulOfContinuousMul` `IsTopologicalSemiring.toContinuousMul` `toContinuousNeg`
`toIsTopologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`to_topologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `toIsSemitopologicalRing` `IsSemitopologicalRing.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`	—	`IsSemitopologicalSemiring.continuousNeg_of_mul`
`toContinuousAdd` 📖	mathematical	—	`ContinuousAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`toContinuousMul` 📖	mathematical	—	`ContinuousMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`toIsSemitopologicalSemiring` 📖	mathematical	—	`IsSemitopologicalSemiring`	—	`toContinuousAdd` `instSeparatelyContinuousMulOfContinuousMul` `toContinuousMul`
`toIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `NonAssocRing.toNonUnitalNonAssocRing`	—	`IsSemitopologicalSemiring.continuousNeg_of_mul` `instSeparatelyContinuousMulOfContinuousMul` `toContinuousMul`

NonUnitalSubring

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsSemitopologicalRing` 📖	mathematical	—	`IsSemitopologicalRing` `NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `toNonUnitalRing`	—	`Subsemigroup.instMulMemClass` `Subsemigroup.separatelyContinuousMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `AddSubgroup.instIsTopologicalAddGroupSubtypeMem` `IsSemitopologicalRing.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `IsTopologicalAddGroup.toContinuousNeg`
`instIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `toNonUnitalRing`	—	`Subsemigroup.instMulMemClass` `Subsemigroup.continuousMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `AddSubgroup.instIsTopologicalAddGroupSubtypeMem` `IsSemitopologicalRing.toIsTopologicalAddGroup` `IsTopologicalRing.toIsSemitopologicalRing` `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`	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`closure_minimal`
`topologicalClosure_mono` 📖	mathematical	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`closure_mono`

NonUnitalSubsemiring

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsSemitopologicalSemiring` 📖	mathematical	—	`IsSemitopologicalSemiring` `NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `instNonUnitalSubsemiringClass`	—	`Subsemigroup.instMulMemClass` `Subsemigroup.separatelyContinuousMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `AddSubmonoid.continuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `instNonUnitalSubsemiringClass`
`instIsTopologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `instNonUnitalSubsemiringClass`	—	`Subsemigroup.instMulMemClass` `Subsemigroup.continuousMul` `IsTopologicalSemiring.toContinuousMul` `AddSubmonoid.continuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `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`	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`closure_minimal`
`topologicalClosure_mono` 📖	mathematical	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`closure_mono`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsSemitopologicalRing` 📖	mathematical	`IsSemitopologicalRing`	`IsSemitopologicalRing` `topologicalSpace` `nonUnitalNonAssocRing`	—	`instIsSemitopologicalSemiring` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `continuousNeg` `IsSemitopologicalRing.toContinuousNeg`
`instIsSemitopologicalSemiring` 📖	mathematical	`IsSemitopologicalSemiring`	`IsSemitopologicalSemiring` `topologicalSpace` `nonUnitalNonAssocSemiring`	—	`continuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `separatelyContinuousMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`instIsTopologicalRing` 📖	mathematical	`IsTopologicalRing`	`IsTopologicalRing` `topologicalSpace` `nonUnitalNonAssocRing`	—	`instIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `continuousNeg` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing`
`instIsTopologicalSemiring` 📖	mathematical	`IsTopologicalSemiring`	`IsTopologicalSemiring` `topologicalSpace` `nonUnitalNonAssocSemiring`	—	`continuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `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	4 math math: `topologicalClosure_minimal`, `le_topologicalClosure`, `topologicalClosure_mono`, `isClosed_topologicalClosure`

Theorems

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

Subsemiring

Definitions

Name	Category	Theorems
`commSemiringTopologicalClosure` 📖	CompOp	—
`topologicalClosure` 📖	CompOp	5 math math: `isClosed_topologicalClosure`, `topologicalClosure_mono`, `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`
`semitopologicalSemiring` 📖	mathematical	—	`IsSemitopologicalSemiring` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toNonAssocSemiring`	—	`Submonoid.separatelyContinuousMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `AddSubmonoid.continuousAdd` `IsSemitopologicalSemiring.toContinuousAdd`
`topologicalClosure_coe` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `Semiring.toNonAssocSemiring` `instSetLike` `topologicalClosure` `closure`	—	—
`topologicalClosure_minimal` 📖	mathematical	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`closure_minimal`
`topologicalClosure_mono` 📖	mathematical	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`closure_mono`
`topologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toNonAssocSemiring`	—	`Submonoid.continuousMul` `IsTopologicalSemiring.toContinuousMul` `AddSubmonoid.continuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring`

(root)

Definitions

Name	Category	Theorems
`IsSemitopologicalRing` 📖	CompData	10 math math: `instIsSemitopologicalRingAddOpposite`, `IsSemitopologicalSemiring.toIsSemitopologicalRing`, `instIsSemitopologicalRingProd`, `NonUnitalStarSubalgebra.instIsSemitopologicalRing`, `NonUnitalSubring.instIsSemitopologicalRing`, `IsTopologicalRing.toIsSemitopologicalRing`, `Pi.instIsSemitopologicalRing`, `instIsSemitopologicalRingMulOpposite`, `NonUnitalSubalgebra.instIsSemitopologicalRing`, `Subring.instIsSemitopologicalRing`
`IsSemitopologicalSemiring` 📖	CompData	12 math math: `Pi.instIsSemitopologicalSemiring`, `instIsSemitopologicalSemiringProd`, `Subsemiring.semitopologicalSemiring`, `IsSemitopologicalRing.toIsSemitopologicalSemiring`, `instIsSemitopologicalSemiringAddOpposite`, `NonUnitalSubsemiring.instIsSemitopologicalSemiring`, `instIsSemitopologicalSemiringMulOpposite`, `StarSubalgebra.instIsSemitopologicalSemiringSubtypeMem`, `NonUnitalSubalgebra.instIsSemitopologicalSemiring`, `NonUnitalStarSubalgebra.instIsSemitopologicalSemiring`, `IsTopologicalSemiring.toIsSemitopologicalSemiring`, `instIsSemitopologicalSemiringSubtypeMemSubalgebra`
`IsTopologicalRing` 📖	CompData	43 math math: `NonUnitalSubring.instIsTopologicalRing`, `IsTopologicalRing.of_nhds_zero`, `MvPowerSeries.WithPiTopology.instIsTopologicalRing`, `RingFilterBasis.isTopologicalRing`, `IsTopologicalSemiring.toIsTopologicalRing`, `instIsTopologicalRingULift`, `RingTopology.toIsTopologicalRing`, `RestrictedProduct.instIsTopologicalRingCoePrincipal`, `IsValuativeTopology.isTopologicalRing`, `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`, `RestrictedProduct.isTopologicalRing`, `NumberField.InfinitePlace.Completion.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`, `Pi.instIsTopologicalRing`, `IsTopologicalRing.of_norm`, `WithIdealFilter.instIsTopologicalRing`, `IsTopologicalRing.of_addGroup_of_nhds_zero`, `UniformSpace.Completion.topologicalRing`
`IsTopologicalSemiring` 📖	CompData	21 math math: `instIsTopologicalSemiringProd`, `Pi.instIsTopologicalSemiring`, `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
`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`
`instIsSemitopologicalRingAddOpposite` 📖	mathematical	—	`IsSemitopologicalRing` `AddOpposite` `AddOpposite.instTopologicalSpaceAddOpposite` `AddOpposite.instNonUnitalNonAssocRing`	—	`instIsSemitopologicalSemiringAddOpposite` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `instContinuousNegAddOpposite` `IsSemitopologicalRing.toContinuousNeg`
`instIsSemitopologicalRingMulOpposite` 📖	mathematical	—	`IsSemitopologicalRing` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instNonUnitalNonAssocRing`	—	`instIsSemitopologicalSemiringMulOpposite` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `instContinuousNegMulOpposite` `IsSemitopologicalRing.toContinuousNeg`
`instIsSemitopologicalRingProd` 📖	mathematical	—	`IsSemitopologicalRing` `instTopologicalSpaceProd` `Prod.instNonUnitalNonAssocRing`	—	`instIsSemitopologicalSemiringProd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `Prod.continuousNeg` `IsSemitopologicalRing.toContinuousNeg`
`instIsSemitopologicalSemiringAddOpposite` 📖	mathematical	—	`IsSemitopologicalSemiring` `AddOpposite` `AddOpposite.instTopologicalSpaceAddOpposite` `AddOpposite.instNonUnitalNonAssocSemiring`	—	`AddOpposite.instContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `instSeparatelyContinuousMulAddOpposite` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`instIsSemitopologicalSemiringMulOpposite` 📖	mathematical	—	`IsSemitopologicalSemiring` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instNonUnitalNonAssocSemiring`	—	`instContinuousAddMulOpposite` `IsSemitopologicalSemiring.toContinuousAdd` `MulOpposite.instSeparatelyContinuousMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`instIsSemitopologicalSemiringProd` 📖	mathematical	—	`IsSemitopologicalSemiring` `instTopologicalSpaceProd` `Prod.instNonUnitalNonAssocSemiring`	—	`Prod.continuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `Prod.separatelyContinuousMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`instIsTopologicalRingAddOpposite` 📖	mathematical	—	`IsTopologicalRing` `AddOpposite` `AddOpposite.instTopologicalSpaceAddOpposite` `AddOpposite.instNonUnitalNonAssocRing`	—	`instIsTopologicalSemiringAddOpposite` `IsTopologicalRing.toIsTopologicalSemiring` `instContinuousNegAddOpposite` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing`
`instIsTopologicalRingMulOpposite` 📖	mathematical	—	`IsTopologicalRing` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instNonUnitalNonAssocRing`	—	`instIsTopologicalSemiringMulOpposite` `IsTopologicalRing.toIsTopologicalSemiring` `instContinuousNegMulOpposite` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing`
`instIsTopologicalRingProd` 📖	mathematical	—	`IsTopologicalRing` `instTopologicalSpaceProd` `Prod.instNonUnitalNonAssocRing`	—	`instIsTopologicalSemiringProd` `IsTopologicalRing.toIsTopologicalSemiring` `Prod.continuousNeg` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing`
`instIsTopologicalRingULift` 📖	mathematical	—	`IsTopologicalRing` `ULift.topologicalSpace` `ULift.nonUnitalNonAssocRing`	—	`instContinuousAddULift` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instContinuousMulULift` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instContinuousNegULift` `IsSemitopologicalRing.toContinuousNeg`
`instIsTopologicalSemiringAddOpposite` 📖	mathematical	—	`IsTopologicalSemiring` `AddOpposite` `AddOpposite.instTopologicalSpaceAddOpposite` `AddOpposite.instNonUnitalNonAssocSemiring`	—	`AddOpposite.instContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `instContinuousMulAddOpposite` `IsTopologicalSemiring.toContinuousMul`
`instIsTopologicalSemiringMulOpposite` 📖	mathematical	—	`IsTopologicalSemiring` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instNonUnitalNonAssocSemiring`	—	`instContinuousAddMulOpposite` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `MulOpposite.instContinuousMul` `IsTopologicalSemiring.toContinuousMul`
`instIsTopologicalSemiringProd` 📖	mathematical	—	`IsTopologicalSemiring` `instTopologicalSpaceProd` `Prod.instNonUnitalNonAssocSemiring`	—	`Prod.continuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `Prod.continuousMul` `IsTopologicalSemiring.toContinuousMul`
`instIsTopologicalSemiringULift` 📖	mathematical	—	`IsTopologicalSemiring` `ULift.topologicalSpace` `ULift.nonUnitalNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`instContinuousAddULift` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `instContinuousMulULift` `IsTopologicalSemiring.toContinuousMul`
`instSeparatelyContinuousMulAddOpposite` 📖	mathematical	—	`SeparatelyContinuousMul` `AddOpposite` `AddOpposite.instTopologicalSpaceAddOpposite` `AddOpposite.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`separatelyContinuousMul_induced` `MulEquivClass.instMulHomClass` `MulEquiv.instMulEquivClass`
`mulLeft_continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddMonoidHom.instFunLike` `AddMonoidHom.mulLeft`	—	`Continuous.const_mul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `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_const` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `continuous_id`

---

← Back to Index