Structures · Analysis
SeminormedRing
A seminormed ring is a 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 by2
Forgetful instances
Concrete types that are instances9
- ContinuousLinearMap
- BoundedContinuousFunction
- TrivSqZeroExt
- RestrictScalars
- Subtype
- Prod
- ULift
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by557
- Bornology.IsVonNBounded
- norm_pow
- Submonoid.unitSphere
- Seminorm.ball
- Balanced
- SeminormFamily
- ContinuousLinearMap.lsmul
- Seminorm.comp
- Seminorm.closedBall
- norm_algebraMap'
- AbsConvex
- Asymptotics.IsBigO.mul
- absConvexHull
- SeminormFamily.basisSets
- balancedCore
- Asymptotics.IsBigO.const_mul_left
- SeminormFamily.basisSets_iff
- Asymptotics.IsBigO.mul_isLittleO
- nnnorm_smul
- Polynomial.supNorm
- tendsto_pow_atTop_nhds_zero_of_norm_lt_one
- spectralValue
- balancedHull
- Asymptotics.IsLittleO.mul_isBigO
- dist_smul₀
- Seminorm.mem_ball_zero
- SeminormedRing.toRingSeminorm
- Seminorm.toAddGroupSeminorm
- closedAbsConvexHull
- Seminorm.mem_ball
- AbsConvexOpenSets
- Asymptotics.IsLittleO.const_mul_left
- nnnorm_pow
- balancedCore_subset
- spectralValueTerms
- Asymptotics.isBigO_const_mul_self
- Absorbs.exists_pos
- normHom
- Seminorm.mem_closedBall
- Asymptotics.IsBigO.pow
- Seminorm.ball_zero_eq
- Seminorm.finset_sup_apply
- Seminorm.IsBounded
- Balanced.smul_mem
- subset_absConvexHull
- nnnormHom
- balancedCore_balanced
- NormedAlgebra.restrictScalars
- balancedCoreAux
- SeminormFamily.basisSets_mem
Ancestors102
- 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
- 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
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NNDist
- NNNorm
- NPow
- NSMul
- NatCast
- Neg
- NegZeroClass
- NonAssocRing
- NonAssocSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Norm
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- Ring
- SMul
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SeminormedAddCommGroup
- SeminormedAddGroup
- Semiring
- SequentialSpace
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZSMul
- Zero