Structures · Analysis
SeminormedCommRing
A seminormed commutative ring is a commutative 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 mul_comm
Extends2
Extended by1
Forgetful instances
Every SeminormedCommRing is also a
Provided automatically by
Concrete types that are instances9
- BoundedContinuousFunction
- TrivSqZeroExt
- RestrictScalars
- Subtype
- Prod
- ULift
- MulOpposite
- HasQuotient.Quotient
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by67
- norm_prod
- MulAlgebraNorm.toMulRingNorm
- AlgebraNorm.toRingNorm
- Asymptotics.IsBigO.multisetProd
- HasProd.norm
- Asymptotics.IsBigO.finsetProd
- nnnorm_prod
- AlgebraNorm.restriction
- AlgebraNorm.extends_norm'
- Filter.boundedFilterSubalgebra
- AlgebraNorm.smul'
- MulAlgebraNorm.toAlgebraNorm
- Multipliable.norm_tprod
- StrongDual.dualPairing_separatingLeft
- MulAlgebraNorm.extends_norm'
- MulAlgebraNorm.coe_AlgebraNorm
- MulAlgebraNorm.smul'
- MulAlgebraNorm.toFun_eq_coe
- AlgebraNorm.extends_norm
- Asymptotics.IsLittleO.multisetProd
- AlgebraNorm.toRingSeminorm'
- Prod.seminormedCommRing
- PiLp.basis_toMatrix_basisFun_mul
- MulAlgebraNorm.mulAlgebraNormClass
- SeparationQuotient.instNormedCommRing
- SeminormedCommRing.toSeminormedRing
- BoundedContinuousFunction.instSeminormedCommRing
- Seminorm.comp_smul_apply
- Filter.BoundedAtFilter.prod
- Ideal.Quotient.norm_mk_le
- MulAlgebraNorm.extends_norm
- Metric.unitSphere.instCommMonoid
- AlgebraNorm.toSeminorm
- Multipliable.norm
- ULift.seminormedCommRing
- Metric.unitClosedBall.instCommMonoid
- SeminormedCommRing.toNonUnitalSeminormedCommRing
- AlgebraNorm.isScalarTower_restriction
- instSeminormedCommRingRestrictScalars
- MulOpposite.instSeminormedCommRing
- Ideal.Quotient.semiNormedCommRing
- MulAlgebraNorm.instFunLikeReal
- Ideal.Quotient.normedCommRing
- MulAlgebraNormClass.toSeminormClass
- Submodule.Quotient.instIsBoundedSMul
- Metric.unitBall.instCommSemigroup
- SubringClass.toSeminormedCommRing
- AlgebraNormClass.toSeminormClass
- ContinuousMap.instSeminormedCommRing
- SeminormedCommRing.toCommRing
Ancestors120
- 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
- CommMagma
- CommMonoid
- CommMonoidWithZero
- CommRing
- CommSemigroup
- CommSemiring
- CompactSpace
- CompactlyCoherentSpace
- Dist
- Distrib
- Dvd
- EDist
- ENorm
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- Ideal.FiniteHeight
- IntCast
- InvolutiveNeg
- IsJacobsonRing
- IsLeftCancelAdd
- IsRightCancelAdd
- IsSemiprimaryRing
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.CommRing
- Lean.Grind.CommSemiring
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Lean.Grind.Ring
- Lean.Grind.Semiring
- LocallyPathConnectedSpace
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NNDist
- NNNorm
- NPow
- NSMul
- NatCast
- Neg
- NegZeroClass
- NonAssocCommRing
- NonAssocCommSemiring
- NonAssocRing
- NonAssocSemiring
- NonUnitalCommRing
- NonUnitalCommSemiring
- NonUnitalNonAssocCommRing
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalRing
- NonUnitalSeminormedCommRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Norm
- 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