Mathlib Map

Theorems · Theorem · functional analysis

star_isometry

∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E], Isometry star

The star map in a normed star group is an isometry

Defined in
Mathlib.Analysis.CStarAlgebra.Basic
Cited by
6 results in Mathlib
Foundations
Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SeminormedAddCommGroupStarAddMonoidNormedStarGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Metric.star_closedBall · cited by 0Metric.star_closedBallMetric.star_sphere · cited by 0Metric.star_sphereedist_star_star · cited by 0edist_star_stardist_star_star · cited by 0dist_star_starnndist_star_star · cited by 0nndist_star_starMetric.star_ball · cited by 0Metric.star_ballDFunLike.coe · cited by 62936DFunLike.coeNorm.norm · cited by 5413Norm.normSeminormedAddCommGroup · cited by 2671SeminormedAddCommGroupStar.star · cited by 1082Star.starStarAddMonoid · cited by 296StarAddMonoidIsometry · cited by 230IsometryNormedStarGroup · cited by 54NormedStarGroupstarAddEquiv · cited by 25starAddEquivAddMonoidHomClass.isometry_of_norm · cited by 18AddMonoidHomClass.isometr…norm_star · cited by 16norm_starstar_isometryCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by6

Results whose statement or proof uses this declaration.