Structures · Analysis
NormOneClass
A mixin class with the axiom ‖1‖ = 1. Many NormedRings and all NormedFields satisfy this
axiom.
- Defined in
- Mathlib.Analysis.Normed.Ring.Basic
- Shape
- One type argument · adds norm_one
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances14
- Int
- SeparationQuotient
- ContinuousLinearMap
- BoundedContinuousFunction
- Quaternion
- Unitization
- Matrix
- PadicInt
- TrivSqZeroExt
- Subtype
- Prod
- ULift
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by170
- NormOneClass.norm_one
- norm_pow
- Submonoid.unitSphere
- norm_algebraMap'
- enorm_one
- Asymptotics.isLittleO_one_iff
- norm_prod
- nnnorm_one
- spectrum.norm_le_norm_of_mem
- Filter.Tendsto.isBigO_one
- nnnorm_pow
- normHom
- Asymptotics.IsBigO.pow
- nnnormHom
- Finset.norm_prod_le
- ContinuousAt.isLittleO
- Asymptotics.isBigO_const_one
- Seminorm.restrictScalars
- multipliable_one_add_of_summable
- algebraMap_isometry
- Filter.IsBoundedUnder.isBigO_one
- FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto
- Summable.hasProdUniformlyOn_one_add
- ContinuousMultilinearMap.norm_mkPiAlgebraFin
- FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto
- Asymptotics.isLittleO_one_left_iff
- nnnorm_algebraMap'
- lpInftySubring
- subset_balancedHull
- Asymptotics.IsBigOWith.pow'
- Submonoid.unitClosedBall
- Asymptotics.isBigOWith_const_one
- IsUltrametricDist.nnnorm_natCast_le_one
- Balanced.neg_mem_iff
- norm_pow_le
- AddChar.norm_apply
- ContinuousMultilinearMap.norm_mkPiAlgebra
- FormalMultilinearSeries.ofScalars_norm
- spectrum.le_nnnorm_of_mem
- List.norm_prod_le
- IsOfFinOrder.norm_eq_one
- Asymptotics.IsBigOWith.of_pow
- summable_finsetProd_of_summable_norm
- Summable.hasProdUniformlyOn_nat_one_add
- AlgEquiv.lpBCF
- Summable.hasProdLocallyUniformlyOn_one_add
- HasProd.norm
- norm_natCast
- nnnorm_prod
- multipliable_norm_one_add_of_summable_norm
Ancestors0
No ancestors.