Structures · Analysis
NormedRing
A normed ring is a 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 NormedRing is also a
Provided automatically by
Concrete types that are instances16
- SeparationQuotient
- ContinuousLinearMap
- BoundedContinuousFunction
- CStarMatrix
- UniformSpace.Completion
- Unitization
- WithLp
- TrivSqZeroExt
- RestrictScalars
- DoubleCentralizer
- Subtype
- Prod
- ULift
- MulOpposite
- ContinuousMap
- WithAbs
How is a type an instance?
Loading the hierarchy index…
Assumed by1,054
- MeasureTheory.Integrable.const_mul
- Asymptotics.IsBigO.mul
- MeasureTheory.Lp.simpleFunc.module
- NormedSpace.expSeries_radius_eq_top
- HasDerivAt.const_mul
- ContinuousMap.toLp
- HasDerivAt.mul
- selfAdjoint.expUnitary
- AnalyticAt.smul
- MeasureTheory.Integrable.mul_const
- CFC.log
- deriv_fun_mul
- Asymptotics.IsBigO.mul_isLittleO
- IntervalIntegrable.const_mul
- MeasureTheory.MemLp.smul
- DifferentiableAt.mul
- MeromorphicAt.smul
- summable_geometric_of_norm_lt_one
- formalMultilinearSeries_geometric
- BoundedContinuousFunction.toLp
- DifferentiableAt.const_mul
- Asymptotics.IsLittleO.mul_isBigO
- MeasureTheory.Lp.coeFn_smul
- MeasureTheory.MemLp.const_smul
- spectrum.norm_le_norm_of_mem
- meromorphicOrderAt_smul
- PowerSeries.IsRestricted
- ContinuousMap.linearIsometryBoundedOfCompact
- AnalyticAt.fun_smul
- Unitary.mulRight
- AnalyticAt.pow
- alternatingGeometricSeries
- Differentiable.mul
- Units.oneSub
- selfAdjoint.expUnitary_coe
- NormedSpace.exp_add_of_commute
- HasDerivAt.mul_const
- spectrum.nonempty
- ContDiff.mul
- Differentiable.const_mul
- MvPowerSeries.IsRestricted
- IntervalIntegrable.continuousOn_mul
- DifferentiableAt.fun_pow
- Asymptotics.IsBigO.pow
- PadicInt.addChar_of_value_at_one
- BoundedContinuousFunction.toContinuousMapStarₐ
- HasFDerivAt.smul
- IntervalIntegrable.mul_continuousOn
- NormedSpace.map_exp
- Unitary.mulLeft
Ancestors108
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommGroupWithOne
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddGroup
- AddGroupWithOne
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddMonoidWithOne
- 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
- IntCast
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- IsSemiprimaryRing
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Lean.Grind.Ring
- Lean.Grind.Semiring
- LocallyPathConnectedSpace
- MetricSpace
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NNDist
- NNNorm
- NPow
- NSMul
- NatCast
- Neg
- NegZeroClass
- NonAssocRing
- NonAssocSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalNormedRing
- NonUnitalRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Norm
- NormedAddCommGroup
- NormedAddGroup
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- Ring
- SMul
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SeminormedAddCommGroup
- SeminormedAddGroup
- SeminormedRing
- Semiring
- SequentialSpace
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZSMul
- Zero