GelfandNaimarkSegal

📁 Source: Mathlib/Analysis/CStarAlgebra/GelfandNaimarkSegal.lean

Statistics

Metric	Count
Definitions GNS, PreGNS, gnsNonUnitalStarAlgHom, gnsStarAlgHom, instAddCommGroupPreGNS, instInnerProductSpaceComplexPreGNS, instModuleComplexPreGNS, instSeminormedAddCommGroupPreGNS, leftMulMapPreGNS, ofPreGNS, preGNSpreInnerProdSpace, toPreGNS	12
Theorems gnsNonUnitalStarAlgHom_apply, gnsNonUnitalStarAlgHom_apply_coe, gnsStarAlgHom_apply, leftMulMapPreGNS_apply, leftMulMapPreGNS_mul_eq_comp, ofPreGNS_toPreGNS, preGNS_inner_def, preGNS_norm_def, preGNS_norm_sq, toPreGNS_ofPreGNS	10
Total	22

PositiveLinearMap

Definitions

Name	Category	Theorems
GNS 📖	CompOp	3 math math: gnsNonUnitalStarAlgHom_apply_coe, gnsStarAlgHom_apply, gnsNonUnitalStarAlgHom_apply
PreGNS 📖	CompOp	10 math math: preGNS_norm_def, leftMulMapPreGNS_apply, gnsNonUnitalStarAlgHom_apply_coe, preGNS_inner_def, toPreGNS_ofPreGNS, gnsStarAlgHom_apply, ofPreGNS_toPreGNS, leftMulMapPreGNS_mul_eq_comp, gnsNonUnitalStarAlgHom_apply, preGNS_norm_sq
gnsNonUnitalStarAlgHom 📖	CompOp	3 math math: gnsNonUnitalStarAlgHom_apply_coe, gnsStarAlgHom_apply, gnsNonUnitalStarAlgHom_apply
gnsStarAlgHom 📖	CompOp	1 math math: gnsStarAlgHom_apply
instAddCommGroupPreGNS 📖	CompOp	10 math math: preGNS_norm_def, leftMulMapPreGNS_apply, gnsNonUnitalStarAlgHom_apply_coe, preGNS_inner_def, toPreGNS_ofPreGNS, gnsStarAlgHom_apply, ofPreGNS_toPreGNS, leftMulMapPreGNS_mul_eq_comp, gnsNonUnitalStarAlgHom_apply, preGNS_norm_sq
instInnerProductSpaceComplexPreGNS 📖	CompOp	4 math math: gnsNonUnitalStarAlgHom_apply_coe, preGNS_inner_def, gnsStarAlgHom_apply, gnsNonUnitalStarAlgHom_apply
instModuleComplexPreGNS 📖	CompOp	10 math math: preGNS_norm_def, leftMulMapPreGNS_apply, gnsNonUnitalStarAlgHom_apply_coe, preGNS_inner_def, toPreGNS_ofPreGNS, gnsStarAlgHom_apply, ofPreGNS_toPreGNS, leftMulMapPreGNS_mul_eq_comp, gnsNonUnitalStarAlgHom_apply, preGNS_norm_sq
instSeminormedAddCommGroupPreGNS 📖	CompOp	8 math math: preGNS_norm_def, leftMulMapPreGNS_apply, gnsNonUnitalStarAlgHom_apply_coe, preGNS_inner_def, gnsStarAlgHom_apply, leftMulMapPreGNS_mul_eq_comp, gnsNonUnitalStarAlgHom_apply, preGNS_norm_sq
leftMulMapPreGNS 📖	CompOp	4 math math: leftMulMapPreGNS_apply, gnsNonUnitalStarAlgHom_apply_coe, leftMulMapPreGNS_mul_eq_comp, gnsNonUnitalStarAlgHom_apply
ofPreGNS 📖	CompOp	6 math math: preGNS_norm_def, leftMulMapPreGNS_apply, preGNS_inner_def, toPreGNS_ofPreGNS, ofPreGNS_toPreGNS, preGNS_norm_sq
preGNSpreInnerProdSpace 📖	CompOp	—
toPreGNS 📖	CompOp	3 math math: leftMulMapPreGNS_apply, toPreGNS_ofPreGNS, ofPreGNS_toPreGNS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gnsNonUnitalStarAlgHom_apply 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom Complex ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring GNS UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace PreGNS PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroupPreGNS ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid UniformSpace.Completion.instNormedAddCommGroup UniformSpace.Completion.instModule SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup instModuleComplexPreGNS IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupPreGNS SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Complex.instNormedField InnerProductSpace.toNormedSpace Complex.instRCLike instInnerProductSpaceComplexPreGNS NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.ring Complex.instRing UniformSpace.Completion.instAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.distribMulAction UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup UniformContinuousConstSMul.to_continuousConstSMul UniformSpace.Completion.instUniformContinuousConstSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.instStarId UniformSpace.Completion.innerProductSpace UniformSpace.Completion.completeSpace NonUnitalStarAlgHom.instFunLike gnsNonUnitalStarAlgHom ContinuousLinearMap.completion leftMulMapPreGNS	—	SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul UniformSpace.Completion.instUniformContinuousConstSMul UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul smulCommClass_self UniformSpace.Completion.completeSpace
gnsNonUnitalStarAlgHom_apply_coe 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring GNS UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace PreGNS PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroupPreGNS ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid UniformSpace.Completion.instNormedAddCommGroup UniformSpace.Completion.instModule SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup instModuleComplexPreGNS IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupPreGNS SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Complex.instNormedField InnerProductSpace.toNormedSpace Complex.instRCLike instInnerProductSpaceComplexPreGNS ContinuousLinearMap.funLike NonUnitalStarAlgHom NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.ring Complex.instRing UniformSpace.Completion.instAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.distribMulAction UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup UniformContinuousConstSMul.to_continuousConstSMul UniformSpace.Completion.instUniformContinuousConstSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.instStarId UniformSpace.Completion.innerProductSpace UniformSpace.Completion.completeSpace NonUnitalStarAlgHom.instFunLike gnsNonUnitalStarAlgHom UniformSpace.Completion.coe' leftMulMapPreGNS	—	SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul UniformSpace.Completion.instUniformContinuousConstSMul UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul smulCommClass_self UniformSpace.Completion.completeSpace RingHomInvPair.ids ContinuousLinearMap.completion_apply_coe
gnsStarAlgHom_apply 📖	mathematical	—	DFunLike.coe StarAlgHom Complex ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring GNS CStarAlgebra.toNonUnitalCStarAlgebra UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace PreGNS PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroupPreGNS ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid UniformSpace.Completion.instNormedAddCommGroup UniformSpace.Completion.instModule SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup instModuleComplexPreGNS IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupPreGNS SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Complex.instNormedField InnerProductSpace.toNormedSpace Complex.instRCLike instInnerProductSpaceComplexPreGNS Complex.instCommSemiring Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid CStarAlgebra.toStarRing ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd UniformSpace.Completion.addGroup SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.algebra UniformSpace.Completion.instAddCommGroup CommSemiring.toSemiring UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid CommRing.toRing Algebra.toSMul Algebra.id UniformSpace.Completion.instIsScalarTower IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul UniformSpace.Completion.instUniformContinuousConstSMul ContinuousLinearMap.instStarId UniformSpace.Completion.innerProductSpace UniformSpace.Completion.completeSpace StarAlgHom.instFunLike gnsStarAlgHom MulActionHom.toFun MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike MonoidHom.id NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace ContinuousLinearMap.ring Complex.instRing ContinuousLinearMap.distribMulAction UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul DistribMulActionHom.toMulActionHom NonUnitalAlgHom.toDistribMulActionHom NonUnitalStarAlgHom.toNonUnitalAlgHom NonUnitalCStarAlgebra.toStarRing gnsNonUnitalStarAlgHom	—	SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul smulCommClass_self UniformSpace.Completion.instIsScalarTower IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul UniformSpace.Completion.instUniformContinuousConstSMul UniformSpace.Completion.completeSpace
leftMulMapPreGNS_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PreGNS UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroupPreGNS AddCommGroup.toAddCommMonoid instAddCommGroupPreGNS instModuleComplexPreGNS ContinuousLinearMap.funLike leftMulMapPreGNS LinearEquiv RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace EquivLike.toFunLike LinearEquiv.instEquivLike toPreGNS Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing ofPreGNS	—	—
leftMulMapPreGNS_mul_eq_comp 📖	mathematical	—	leftMulMapPreGNS Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ContinuousLinearMap.comp Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PreGNS UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroupPreGNS AddCommGroup.toAddCommMonoid instAddCommGroupPreGNS instModuleComplexPreGNS RingHomCompTriple.ids	—	ContinuousLinearMap.ext RingHomCompTriple.ids RingHomInvPair.ids mul_assoc
ofPreGNS_toPreGNS 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PreGNS AddCommGroup.toAddCommMonoid instAddCommGroupPreGNS ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup instModuleComplexPreGNS NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ofPreGNS toPreGNS	—	RingHomInvPair.ids
preGNS_inner_def 📖	mathematical	—	Inner.inner Complex PreGNS InnerProductSpace.toInner Complex.instRCLike instSeminormedAddCommGroupPreGNS instInnerProductSpaceComplexPreGNS DFunLike.coe PositiveLinearMap Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex Complex.instNormedAddCommGroup Complex.partialOrder NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace Complex.instModuleSelf instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid instAddCommGroupPreGNS instModuleComplexPreGNS EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ofPreGNS	—	—
preGNS_norm_def 📖	mathematical	—	Norm.norm PreGNS SeminormedAddCommGroup.toNorm instSeminormedAddCommGroupPreGNS Real.sqrt Complex.re DFunLike.coe PositiveLinearMap Complex Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex Complex.instNormedAddCommGroup Complex.partialOrder NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace Complex.instModuleSelf instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid instAddCommGroupPreGNS instModuleComplexPreGNS EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ofPreGNS	—	—
preGNS_norm_sq 📖	mathematical	—	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm PreGNS SeminormedAddCommGroup.toNorm instSeminormedAddCommGroupPreGNS DFunLike.coe PositiveLinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex Complex.instNormedAddCommGroup Complex.partialOrder NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace Complex.instModuleSelf instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid instAddCommGroupPreGNS instModuleComplexPreGNS EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ofPreGNS	—	RingHomInvPair.ids map_nonneg instOrderHomClass AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass instLinearMapClass star_mul_self_nonneg preGNS_norm_def Complex.ofReal_pow Real.sq_sqrt Complex.re_nonneg_iff_nonneg LE.le.isSelfAdjoint RCLike.toStarOrderedRing Complex.conj_eq_iff_re LE.le.star_eq
toPreGNS_ofPreGNS 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PreGNS ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup AddCommGroup.toAddCommMonoid instAddCommGroupPreGNS NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace instModuleComplexPreGNS EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toPreGNS ofPreGNS	—	RingHomInvPair.ids

---

← Back to Index