Structures · Topology
IsTopologicalSemiring
A topological semiring is a semiring R where addition and multiplication are continuous.
We allow for non-unital and non-associative semirings as well.
The IsTopologicalSemiring class should only be instantiated in the presence of a
NonUnitalNonAssocSemiring instance; if there is an instance of NonUnitalNonAssocRing,
then IsTopologicalRing should be used. Note: in the presence of NonAssocRing, these classes are
mathematically equivalent (see IsTopologicalSemiring.continuousNeg_of_mul or
IsTopologicalSemiring.toIsTopologicalRing).
- Defined in
- Mathlib.Topology.Algebra.Ring.Basic
- Shape
- One type argument
Extends2
Extended by1
Concrete types that are instances11
- SeparationQuotient
- NNReal
- NNRat
- Matrix
- ENat
- Subtype
- Prod
- ULift
- MulOpposite
- AddOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by514
- cfc
- cfcₙ
- cfcHom
- cfcₙHom
- Summable.mul_left
- cfc_apply
- cfcₙ_apply
- cfcₙ_apply_of_not_predicate
- cfcₙ_congr
- HasSum.mul_left
- cfc_comp'
- tsum_mul_left
- cfc_id
- cfc_congr
- cfcₙ_id
- cfc_apply_of_not_predicate
- MvPowerSeries.aeval
- Subalgebra.SeparatesPoints
- HasSum.div_const
- cfc_id'
- polynomialFunctions
- ContinuousMap.idealOfSet
- cfc.congr_simp
- cfcₙ_apply_of_not_map_zero
- ContinuousMap.compStarAlgHom'
- Polynomial.toContinuousMapOnAlgHom
- cfcₙ_eq_cfc
- cfcHom_continuous
- cfc_const
- cfc_cases
- ContinuousMap.setOfIdeal
- Polynomial.continuous
- cfc_map_spectrum
- cfcHom_id
- PowerSeries.aeval
- cfcₙHom_continuous
- HasSum.mul_right
- cfc_apply_of_not_continuousOn
- cfcₙ_id'
- cfcₙ_comp'
- QuasispectrumRestricts.nonUnitalStarAlgHom
- SpectrumRestricts.starAlgHom
- cfcₙHom_id
- cfcₙ_apply_of_not_continuousOn
- cfcₙ_mul
- cfcₙ_cases
- ContinuousMapZero.toContinuousMapHom
- Polynomial.toContinuousMapOn
- MvPowerSeries.coe_aeval
- cfcₙ.congr_simp