Structures · Analysis
NonUnitalNormedRing
A non-unital normed ring is a not-necessarily-unital ring
endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.
- Defined in
- Mathlib.Analysis.Normed.Ring.Basic
- Shape
- One type argument · adds dist_eq, norm_mul_le
Extends3
Extended by3
Forgetful instances
Every NonUnitalNormedRing is also a
Provided automatically by
Concrete types that are instances10
- SeparationQuotient
- BoundedContinuousFunction
- CStarMatrix
- RestrictScalars
- ZeroAtInftyContinuousMap
- Subtype
- Prod
- ULift
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by326
- DoubleCentralizer.toProd
- CStarRing.norm_star_mul_self
- cfcₙAux
- Unitization.normedRingAux
- compactlySupported
- Unitization.norm_inr
- Unitization.isometry_inr
- Unitization.splitMul
- IsGreatest.nnnorm_cfcₙ_nnreal
- IsGreatest.norm_cfcₙ
- WithLp.unitizationAlgEquiv
- Unitization.norm_eq_sup
- norm_apply_le_norm_cfcₙ
- DoubleCentralizer.coe
- CStarRing.nnnorm_star_mul_self
- DoubleCentralizer.toProdMulOpposite
- CStarRing.norm_self_mul_star
- apply_le_nnnorm_cfcₙ_nnreal
- cfcₙAux_id
- quasispectrum.isCompact
- ContinuousOn.cfcₙ_nnreal
- Unitization.splitMul_apply
- CStarAlgebra.norm_posPart_le
- continuous_cfcₙAux
- DoubleCentralizer.norm_fst_eq_snd
- norm_cfcₙ_le
- ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet
- CFC.norm_star_mul_mul_self_of_nonneg
- mem_compactlySupported
- DoubleCentralizer.toProdHom
- CFC.nnnorm_nnrpow
- upperHemicontinuous_quasispectrum
- ContinuousOn.cfcₙ
- DoubleCentralizer.toProdMulOppositeHom
- IsGreatest.nnnorm_cfcₙ
- DoubleCentralizer.central
- continuousOn_cfcₙ
- Filter.Tendsto.cfcₙ_nnreal
- cfcₙ_setIntegral
- RCLike.nonUnitalContinuousFunctionalCalculus
- norm_cfcₙ_lt
- upperHemicontinuous_quasispectrum_nnreal
- cfcₙL_integral
- IsSelfAdjoint.norm_mul_self
- integrable_cfcₙ'
- Unitization.continuous_inr
- cfcₙ_integral'
- Unitization.antilipschitzWith_addEquiv
- WithLp.unitization_norm_def
- Dilation.mulRight
Ancestors85
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- AlgebraicGeometry.QuasiSeparated
- Bornology
- Bracket
- ChartedSpace
- CompactSpace
- CompactlyCoherentSpace
- Dist
- Distrib
- Dvd
- EDist
- EMetricSpace
- ENorm
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- LocallyPathConnectedSpace
- MetricSpace
- Mul
- MulZeroClass
- NNDist
- NNNorm
- NSMul
- Neg
- NegZeroClass
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Norm
- NormedAddCommGroup
- NormedAddGroup
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- SMul
- Semigroup
- SemigroupWithZero
- SeminormedAddCommGroup
- SeminormedAddGroup
- SequentialSpace
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZSMul
- Zero