Theorems · Theorem · functional analysis

CStarModule.norm_eq_sqrt_norm_inner_self

∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] (x : E), ‖x‖ = √‖inner A x x‖

Defined in

Mathlib.Analysis.CStarAlgebra.Module.Defs

Cited by

10 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CStarModule