Structures · Analysis
NormedStarGroup
A normed star group is a normed group with a compatible star which is isometric.
- Defined in
- Mathlib.Analysis.CStarAlgebra.Basic
- Shape
- One type argument · adds norm_star_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- BoundedContinuousFunction
- Matrix
- ZeroAtInftyContinuousMap
- Subtype
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by81
- norm_star
- BoundedContinuousFunction.toContinuousMapStarₐ
- starₗᵢ
- star_isometry
- nnnorm_star
- HasDerivAt.star_conj
- realPart.norm_le
- HasFDerivAt.star_star
- MeasureTheory.eLpNorm_star
- differentiableAt_star_conj_iff
- ContinuousLinearMap.opNorm_mul_flip_apply
- DifferentiableAt.star_star
- deriv_star_conj
- DoubleCentralizer.coeHom
- hasDerivAt_star_conj_iff
- imaginaryPart.norm_le
- Matrix.nnnorm_conjTranspose
- BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply
- Matrix.frobenius_nnnorm_conjTranspose
- DifferentiableAt.star_conj
- Memℓp.star_mem
- differentiableAt_conj_conj_iff
- NormedStarGroup.norm_star_le
- NormedStarGroup.to_continuousStar
- ZeroAtInftyContinuousMap.instNormedStarGroup
- hasDerivAt_conj_conj_iff
- lp.instStarModuleSubtypePreLpMemAddSubgroup
- Matrix.norm_conjTranspose
- lp.star_apply
- Matrix.frobenius_norm_conjTranspose
- DoubleCentralizer.instStar
- lp.inftyCStarRing
- DoubleCentralizer.star_snd
- Matrix.instNormedStarGroup
- coe_starₗᵢ
- ContinuousLinearMap.opNNNorm_mul_flip_apply
- deriv_conj_conj
- Metric.star_sphere
- edist_star_star
- BoundedContinuousFunction.coe_toContinuousMapStarₐ
- MeasureTheory.Lp.coeFn_star
- symm_starₗᵢ
- BoundedContinuousFunction.instNormedStarGroup
- lp.inftyStarRing
- RingHomIsometric.starRingEnd
- MeasureTheory.AEEqFun.eLpNorm_star
- Metric.star_ball
- HasDerivAt.conj_conj
- lp.instStarAddMonoid
- MeasureTheory.Lp.instStarSubtypeAEEqFunMemAddSubgroup
Ancestors0
No ancestors.