Theorems · Inductive type · functional analysis
NormedStarGroup
(E : Type u_1) → [inst : SeminormedAddCommGroup E] → [StarAddMonoid E] → Prop
A normed star group is a normed group with a compatible star which is isometric.
- Defined in
- Mathlib.Analysis.CStarAlgebra.Basic
- Cited by
- 54 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SeminormedAddCommGroupstatement · cited by 2,671
- StarAddMonoidstatement · cited by 296
Cited by60
Results whose statement or proof uses this declaration.
- norm_starstatement and proof · cited by 16
- BoundedContinuousFunction.toContinuousMapStarₐstatement and proof · cited by 7
- star_isometrystatement and proof · cited by 6
- starₗᵢstatement and proof · cited by 6
- nnnorm_starstatement and proof · cited by 4
- HasDerivAt.star_conjstatement and proof · cited by 3
- realPart.norm_lestatement and proof · cited by 2
- HasFDerivAt.star_starstatement and proof · cited by 2
- DifferentiableAt.star_starstatement and proof · cited by 2
- MeasureTheory.eLpNorm_starstatement and proof · cited by 2
- ContinuousLinearMap.opNorm_mul_flip_applystatement and proof · cited by 2
- differentiableAt_star_conj_iffstatement and proof · cited by 2