Structures · Topology
IsSemitopologicalRing
A semitopological ring is a ring R where addition is jointly continuous and
multiplication is continuous in each variable separately, and negation is continuous as well.
We allow for non-unital and non-associative rings as well.
If R is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with -1. (See IsTopologicalSemiring.continuousNeg_of_mul
and IsSemitopologicalSemiring.toIsSemitopologicalRing)
- Defined in
- Mathlib.Topology.Algebra.Ring.Basic
- Shape
- One type argument
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- ContinuousLinearMapWOT
- Subtype
- Prod
- MulOpposite
- AddOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by151
- CFC.sqrt_mul_sqrt_self
- cfcₙ_nnreal_eq_real
- cfc_nnreal_eq_real
- CFC.sqrt_eq_iff
- CFC.sqrt_eq_rpow
- CStarAlgebra.isStrictlyPositive_TFAE
- CStarAlgebra.nonneg_TFAE
- CFC.rpow_rpow
- CFC.nnrpow_eq_rpow
- CFC.sqrt_eq_cfc
- CFC.nnrpow_nnrpow
- CFC.sqrt_mul_self
- CFC.sqrt_one
- Subring.topologicalClosure
- NonUnitalSubring.topologicalClosure
- ContinuousOn.cfcₙ_nnreal
- CStarAlgebra.nonneg_iff_eq_star_mul_self
- ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet
- ContinuousOn.cfc_nnreal
- Filter.Tendsto.cfc_nnreal
- CFC.nnrpow_map_prod
- Filter.Tendsto.cfcₙ_nnreal
- ContinuousOn.cfc_nnreal_of_mem_nhdsSet
- Commute.cfcHom
- mulLeft_continuous
- continuousOn_cfc_nnreal
- CFC.sqrt_nnrpow
- CFC.sqrt_eq_real_sqrt
- Commute.cfc
- CFC.nnrpow_map_pi
- continuousOn_cfcₙ_nnreal
- CFC.sqrt_unique
- CFC.rpow_eq_cfc_real
- CFC.conjSqrt_conjSqrt_ringInverse
- ContinuousWithinAt.cfcₙ_nnreal
- CFC.isUnit_sqrt_iff_isStrictlyPositive
- Subalgebra.topologicalClosure_comap_homeomorph
- CFC.nnrpow_inv_nnrpow
- CFC.isUnit_nnrpow_iff
- CFC.ringInverse_conjSqrt
- CFC.mul_self_eq
- CFC.nnrpow_nnrpow_inv
- CFC.isUnit_sqrt_iff
- CFC.rpow_map_pi
- IsStrictlyPositive.sqrt
- CFC.rpow_rpow_inv
- CFC.rpow_map_prod
- ContinuousWithinAt.cfc_nnreal
- CFC.sq_sqrt
- continuousOn_cfcₙ_nnreal_setProd