Structures · Topology
IsTopologicalRing
A topological ring is a ring R where addition, multiplication and negation are continuous.
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 IsTopologicalSemiring.toIsTopologicalRing)
- Defined in
- Mathlib.Topology.Algebra.Ring.Basic
- Shape
- One type argument
Extends2
Extended by2
Concrete types that are instances21
- Real
- Rat
- TopCat.carrier
- SeparationQuotient
- UniformSpace.Completion
- Matrix
- RestrictedProduct
- TrivSqZeroExt
- Localization
- NumberField.InfiniteAdeleRing
- IsDedekindDomain.FiniteAdeleRing
- NumberField.AdeleRing
- TopCommRingCat.α
- WithIdealFilter
- Subtype
- Prod
- ULift
- MulOpposite
- AddOpposite
- HasQuotient.Quotient
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by489
- NormedSpace.exp
- FormalMultilinearSeries.ofScalars
- NormedSpace.expSeries
- AbstractMeasure
- MvPowerSeries.aeval
- ordinaryHypergeometricSeries
- NormedSpace.exp_eq_tsum
- NormedSpace.expSeries_apply_eq
- binomialSeries
- PowerSeries.aeval
- QuasispectrumRestricts.nonUnitalStarAlgHom
- NormedSpace.exp.congr_simp
- VectorFourier.fourierIntegral_convergent_iff
- MvPowerSeries.coe_aeval
- Ideal.closure
- FormalMultilinearSeries.ofScalarsSum
- WeakDual.gelfandTransform
- NormedSpace.exp_zero
- affineHomeomorph
- NormedSpace.exp_eq_expSeries_sum
- Continuous.matrix_det
- cfc_le_iff
- CommRingCat.HomTopology.mvPolynomialHomeomorph
- UniformSpace.Completion.mapRingHom
- UniformSpace.Completion.coe_mul
- LinearMap.toContPerfPair
- FormalMultilinearSeries.ofScalars.congr_simp
- CFC.abs_mul_abs
- affineHomeomorph_apply
- MvPowerSeries.coe_eval₂Hom
- AbstractMeasure.prodMk
- AbstractMeasure.prodMk'
- iccHomeoI
- AbstractMeasure.contractFst
- QuasispectrumRestricts.cfcₙHom_eq_restrict
- AbstractMeasure.contractSnd
- cfc_sub
- NormedSpace.star_exp
- FormalMultilinearSeries.ofScalars_apply_eq
- ContinuousMap.prodMul
- MvPowerSeries.continuous_eval₂
- AbstractMeasure.dirac
- SeparatingDual.exists_eq_one
- QuasispectrumRestricts.nonUnitalStarAlgHom_apply
- NormedSpace.exp_eq_tsum_rat
- CFC.abs_eq_cfcₙ_coe_norm
- AbstractMeasure.map
- MvPowerSeries.eval₂Hom
- Commute.exp_right
- MvPowerSeries.continuous_aeval