Structures · Analysis
NonUnitalSeminormedRing
A non-unital seminormed ring is a not-necessarily-unital ring
endowed with a seminorm 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 NonUnitalSeminormedRing is also a
Provided automatically by
Concrete types that are instances8
- BoundedContinuousFunction
- RestrictScalars
- ZeroAtInftyContinuousMap
- Subtype
- Prod
- ULift
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by87
- ContinuousLinearMap.mul
- norm_mul_le
- ContinuousLinearMap.mulLeftRight
- nnnorm_mul_le
- ContinuousLinearMap.isometry_mul
- ContinuousMap.norm_add_eq_max
- BoundedContinuousFunction.norm_add_eq_max
- ContinuousLinearMap.mul_apply'
- ContinuousLinearMap.opNorm_mul_apply
- Matrix.linfty_opNNNorm_mulVec
- Matrix.linfty_opNNNorm_mul
- NonUnitalAlgHom.Lmul
- ContinuousLinearMap.opNorm_mul_apply_le
- ContinuousLinearMap.mulₗᵢ
- Filter.Tendsto.zero_mul_isBoundedUnder_le
- ContinuousMap.nnnorm_add_eq_max
- BoundedContinuousFunction.norm_sub_eq_max
- nnnorm_mul_le_of_le
- Subsemigroup.unitBall
- Filter.isBoundedUnder_le_mul_tendsto_zero
- ContinuousLinearMap.opNorm_mulLeftRight_apply_le
- NonUnitalSeminormedRing.norm_mul_le
- BoundedContinuousFunction.nnnorm_add_eq_max
- norm_mul₃_le
- ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le
- ContinuousMap.norm_sub_eq_max
- norm_mul_le_of_le
- ContinuousLinearMap.opNorm_mul_le
- Subsemigroup.unitClosedBall
- Metric.unitBall.instSemigroup
- instNonUnitalSeminormedRingRestrictScalars
- NonUnitalSeminormedRing.isBoundedSMul
- ULift.nonUnitalSeminormedRing
- Matrix.linfty_opNorm_mul
- NonUnitalSeminormedRing.toSeminormedAddCommGroup
- Metric.unitClosedBall.instSemigroupWithZero
- ContinuousLinearMap.opNNNorm_mul_apply
- BoundedContinuousFunction.nnnorm_sum_eq_sup
- Metric.unitBall.instHasDistribNeg
- mulLeft_bound
- ContinuousMap.nnnorm_sub_eq_max
- ContinuousLinearMap.mulLeftRight_apply
- NonUnitalSeminormedRing.induced
- MulOpposite.instNonUnitalSeminormedRing
- ContinuousLinearMap.mul.congr_simp
- BoundedContinuousFunction.instSMulCommClass_2
- NonUnitalSeminormedRing.isBoundedSMulOpposite
- SeparationQuotient.instNonUnitalNormedRing
- nnnorm_mul₃_le
- NonUnitalAlgHom.coe_Lmul
Ancestors80
- 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
- ENorm
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- LocallyPathConnectedSpace
- Mul
- MulZeroClass
- NNDist
- NNNorm
- NSMul
- Neg
- NegZeroClass
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalRing
- NonUnitalSemiring
- Nonempty
- Norm
- 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