CStarMatrix

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

Statistics

Metric	Count
Definitions CStarMatrix, conjTranspose, instAdd, instAddCommGroup, instAddCommGroupWithOne, instAddCommMonoid, instAddCommMonoidWithOne, instAddCommSemigroup, instAddGroup, instAddGroupWithOne, instAddMonoid, instAddMonoidWithOne, instAddSemigroup, instAddZeroClass, instAlgebra, instBornology, instCStarAlgebra, instDecidableEq, instDistribMulAction, instFintypeOfDecidableEq, instHMulOfFintypeOfMulOfAddCommMonoid, instInhabited, instInvolutiveStar, instModule, instMulAction, instMulOfFintypeOfAddCommMonoid, instNeg, instNonAssocRing, instNonAssocSemiring, instNonUnitalCStarAlgebra, instNonUnitalNonAssocRing, instNonUnitalNonAssocSemiring, instNonUnitalNormedRing, instNonUnitalRing, instNonUnitalSemiring, instNorm, instNormedAddCommGroup, instNormedAlgebra, instNormedRing, instNormedSpace, instOne, instPartialOrder, instRing, instSMul, instSemiring, instStar, instStarAddMonoid, instStarRing, instSub, instTopologicalSpace, instUniformSpace, instUnique, instZero, map, mapₗ, mapₙₐ, ofMatrix, ofMatrixL, ofMatrixRingEquiv, ofMatrixStarAlgEquiv, ofMatrixₗ, reindexₐ, reindexₗ, toCLM, toCLMNonUnitalAlgHom, toOneByOne, transpose	67
Theorems add_apply, add_mul, algebraMap_apply, conjTranspose_apply, conjTranspose_zero, ext, ext_iff, inner_toCLM_conjTranspose_left, inner_toCLM_conjTranspose_right, instCStarRing, instCompleteSpace, instContinuousSMul, instFinite, instIsCentralScalar, instIsScalarTower, instIsTopologicalAddGroup, instIsUniformAddGroup, instNontrivial, instSMulCommClass, instStarModule, instStarOrderedRing, instSubsingleton, instT2Space, instT3Space, map_apply, map_id, map_id', map_injective, map_map, mapₗ_apply, mapₗ_reindexₐ, mapₙₐ_apply, mul_add, mul_apply, mul_apply', mul_entry_mul_eq_inner_toCLM, mul_smul, mul_zero, neg_apply, neg_of, norm_def, norm_def', norm_entry_le_norm, norm_le_of_forall_inner_le, normedSpaceCore, ofMatrix_apply, ofMatrix_eq_ofMatrixL, ofMatrix_eq_ofMatrixStarAlgEquiv, ofMatrix_symm_apply, of_add_of, of_sub_of, of_zero, one_apply, one_apply_eq, one_apply_ne, one_apply_ne', reindexₐ_apply, reindexₐ_symm, reindexₗ_apply, smul_apply, smul_mul, smul_of, star_apply, star_apply_of_isSelfAdjoint, star_eq_conjTranspose, sub_apply, toCLMNonUnitalAlgHom_eq_toCLM, toCLM_apply, toCLM_apply_eq_sum, toCLM_apply_single, toCLM_apply_single_apply, toCLM_injective, transpose_apply, uniformEmbedding_ofMatrix, zero_apply, zero_mul	76
Total	143

CStarMatrix

Definitions

Name	Category	Theorems
conjTranspose 📖	CompOp	3 math math: conjTranspose_apply, conjTranspose_zero, star_eq_conjTranspose
instAdd 📖	CompOp	8 math math: mapₗ_reindexₐ, mul_add, reindexₐ_apply, add_apply, reindexₐ_symm, ofMatrix_eq_ofMatrixStarAlgEquiv, of_add_of, add_mul
instAddCommGroup 📖	CompOp	1 math math: normedSpaceCore
instAddCommGroupWithOne 📖	CompOp	—
instAddCommMonoid 📖	CompOp	15 math math: mapₗ_reindexₐ, toCLM_injective, inner_toCLM_conjTranspose_left, toCLMNonUnitalAlgHom_eq_toCLM, toCLM_apply_single, toCLM_apply_eq_sum, ofMatrix_eq_ofMatrixL, toCLM_apply, mul_entry_mul_eq_inner_toCLM, reindexₗ_apply, mapₙₐ_apply, mapₗ_apply, norm_def, inner_toCLM_conjTranspose_right, toCLM_apply_single_apply
instAddCommMonoidWithOne 📖	CompOp	—
instAddCommSemigroup 📖	CompOp	—
instAddGroup 📖	CompOp	2 math math: instIsUniformAddGroup, instIsTopologicalAddGroup
instAddGroupWithOne 📖	CompOp	—
instAddMonoid 📖	CompOp	—
instAddMonoidWithOne 📖	CompOp	—
instAddSemigroup 📖	CompOp	—
instAddZeroClass 📖	CompOp	—
instAlgebra 📖	CompOp	1 math math: algebraMap_apply
instBornology 📖	CompOp	—
instCStarAlgebra 📖	CompOp	—
instDecidableEq 📖	CompOp	—
instDistribMulAction 📖	CompOp	3 math math: norm_def', toCLMNonUnitalAlgHom_eq_toCLM, mapₙₐ_apply
instFintypeOfDecidableEq 📖	CompOp	—
instHMulOfFintypeOfMulOfAddCommMonoid 📖	CompOp	8 math math: mul_smul, zero_mul, mul_add, mul_apply, mul_zero, smul_mul, mul_apply', add_mul
instInhabited 📖	CompOp	—
instInvolutiveStar 📖	CompOp	—
instModule 📖	CompOp	16 math math: mapₗ_reindexₐ, toCLM_injective, inner_toCLM_conjTranspose_left, toCLMNonUnitalAlgHom_eq_toCLM, toCLM_apply_single, toCLM_apply_eq_sum, ofMatrix_eq_ofMatrixL, toCLM_apply, mul_entry_mul_eq_inner_toCLM, reindexₗ_apply, normedSpaceCore, mapₙₐ_apply, mapₗ_apply, norm_def, inner_toCLM_conjTranspose_right, toCLM_apply_single_apply
instMulAction 📖	CompOp	—
instMulOfFintypeOfAddCommMonoid 📖	CompOp	4 math math: mapₗ_reindexₐ, reindexₐ_apply, reindexₐ_symm, ofMatrix_eq_ofMatrixStarAlgEquiv
instNeg 📖	CompOp	2 math math: neg_of, neg_apply
instNonAssocRing 📖	CompOp	—
instNonAssocSemiring 📖	CompOp	—
instNonUnitalCStarAlgebra 📖	CompOp	—
instNonUnitalNonAssocRing 📖	CompOp	—
instNonUnitalNonAssocSemiring 📖	CompOp	3 math math: norm_def', toCLMNonUnitalAlgHom_eq_toCLM, mapₙₐ_apply
instNonUnitalNormedRing 📖	CompOp	1 math math: instCStarRing
instNonUnitalRing 📖	CompOp	—
instNonUnitalSemiring 📖	CompOp	1 math math: instStarOrderedRing
instNorm 📖	CompOp	5 math math: norm_entry_le_norm, norm_def', norm_le_of_forall_inner_le, normedSpaceCore, norm_def
instNormedAddCommGroup 📖	CompOp	—
instNormedAlgebra 📖	CompOp	—
instNormedRing 📖	CompOp	—
instNormedSpace 📖	CompOp	—
instOne 📖	CompOp	4 math math: one_apply, one_apply_ne, one_apply_ne', one_apply_eq
instPartialOrder 📖	CompOp	1 math math: instStarOrderedRing
instRing 📖	CompOp	—
instSMul 📖	CompOp	13 math math: mapₗ_reindexₐ, mul_smul, instContinuousSMul, reindexₐ_apply, smul_of, instIsCentralScalar, smul_mul, reindexₐ_symm, ofMatrix_eq_ofMatrixStarAlgEquiv, instSMulCommClass, smul_apply, instStarModule, instIsScalarTower
instSemiring 📖	CompOp	1 math math: algebraMap_apply
instStar 📖	CompOp	8 math math: mapₗ_reindexₐ, star_apply, reindexₐ_apply, reindexₐ_symm, ofMatrix_eq_ofMatrixStarAlgEquiv, star_eq_conjTranspose, instStarModule, mapₙₐ_apply
instStarAddMonoid 📖	CompOp	—
instStarRing 📖	CompOp	2 math math: instStarOrderedRing, instCStarRing
instSub 📖	CompOp	2 math math: sub_apply, of_sub_of
instTopologicalSpace 📖	CompOp	5 math math: instContinuousSMul, ofMatrix_eq_ofMatrixL, instIsTopologicalAddGroup, instT2Space, instT3Space
instUniformSpace 📖	CompOp	3 math math: instIsUniformAddGroup, instCompleteSpace, uniformEmbedding_ofMatrix
instUnique 📖	CompOp	—
instZero 📖	CompOp	5 math math: zero_mul, zero_apply, mul_zero, conjTranspose_zero, of_zero
map 📖	CompOp	8 math math: CompletelyPositiveMapClass.map_cstarMatrix_nonneg', CompletelyPositiveMap.map_cstarMatrix_nonneg, map_id', map_injective, CompletelyPositiveMap.map_cstarMatrix_nonneg', map_id, mapₗ_apply, map_apply
mapₗ 📖	CompOp	3 math math: mapₗ_reindexₐ, mapₙₐ_apply, mapₗ_apply
mapₙₐ 📖	CompOp	1 math math: mapₙₐ_apply
ofMatrix 📖	CompOp	10 math math: ofMatrix_apply, of_sub_of, ofMatrix_eq_ofMatrixL, smul_of, ofMatrix_symm_apply, ofMatrix_eq_ofMatrixStarAlgEquiv, neg_of, uniformEmbedding_ofMatrix, of_zero, of_add_of
ofMatrixL 📖	CompOp	1 math math: ofMatrix_eq_ofMatrixL
ofMatrixRingEquiv 📖	CompOp	—
ofMatrixStarAlgEquiv 📖	CompOp	1 math math: ofMatrix_eq_ofMatrixStarAlgEquiv
ofMatrixₗ 📖	CompOp	—
reindexₐ 📖	CompOp	3 math math: mapₗ_reindexₐ, reindexₐ_apply, reindexₐ_symm
reindexₗ 📖	CompOp	1 math math: reindexₗ_apply
toCLM 📖	CompOp	10 math math: toCLM_injective, inner_toCLM_conjTranspose_left, toCLMNonUnitalAlgHom_eq_toCLM, toCLM_apply_single, toCLM_apply_eq_sum, toCLM_apply, mul_entry_mul_eq_inner_toCLM, norm_def, inner_toCLM_conjTranspose_right, toCLM_apply_single_apply
toCLMNonUnitalAlgHom 📖	CompOp	2 math math: norm_def', toCLMNonUnitalAlgHom_eq_toCLM
toOneByOne 📖	CompOp	—
transpose 📖	CompOp	1 math math: transpose_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	CStarMatrix instAdd	—	—
add_mul 📖	mathematical	—	CStarMatrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid instAdd Distrib.toAdd	—	Matrix.add_mul
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom CStarMatrix Semiring.toNonAssocSemiring CommSemiring.toSemiring instSemiring RingHom.instFunLike algebraMap instAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
conjTranspose_apply 📖	mathematical	—	conjTranspose Star.star	—	—
conjTranspose_zero 📖	mathematical	—	conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar CStarMatrix instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	ext star_zero
ext 📖	—	—	—	—	ext_iff
ext_iff 📖	—	—	—	—	—
inner_toCLM_conjTranspose_left 📖	mathematical	—	Inner.inner WithCStarModule CStarModule.toInner NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing NonUnitalCStarAlgebra.toStarRing NormedSpace.toModule Complex Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNormedSpace WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup WithCStarModule.instModule Complex.instSemiring Pi.module ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instSMul Pi.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNorm WithCStarModule.instNormForall WithCStarModule.instCStarModule WithCStarModule.instCStarModuleForall DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring WithCStarModule.instUniformSpace Pi.uniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace WithCStarModule.instNormedAddCommGroupForall AddCommGroup.toAddCommMonoid Pi.Function.module ContinuousLinearMap.funLike LinearMap CStarMatrix instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM Matrix.conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul toCLM_apply_eq_sum Finset.sum_congr star_sum StarMul.star_mul star_star Finset.mul_sum Finset.sum_mul Finset.sum_comm mul_assoc
inner_toCLM_conjTranspose_right 📖	mathematical	—	Inner.inner WithCStarModule CStarModule.toInner NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing NonUnitalCStarAlgebra.toStarRing NormedSpace.toModule Complex Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNormedSpace WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup WithCStarModule.instModule Complex.instSemiring Pi.module ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instSMul Pi.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNorm WithCStarModule.instNormForall WithCStarModule.instCStarModule WithCStarModule.instCStarModuleForall DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring WithCStarModule.instUniformSpace Pi.uniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace WithCStarModule.instNormedAddCommGroupForall AddCommGroup.toAddCommMonoid Pi.Function.module ContinuousLinearMap.funLike LinearMap CStarMatrix instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM Matrix.conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Matrix.conjTranspose_conjTranspose inner_toCLM_conjTranspose_left
instCStarRing 📖	mathematical	—	CStarRing CStarMatrix instNonUnitalNormedRing instStarRing NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing NonUnitalCStarAlgebra.toStarRing	—	CStarRing.of_le_norm_mul_star_self WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.opNorm_le_iff RingHomIsometric.ids Real.sqrt_nonneg CStarModule.norm_eq_sqrt_norm_inner_self inner_toCLM_conjTranspose_right RingHomCompTriple.ids CStarModule.norm_inner_le mul_assoc mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing ContinuousLinearMap.comp_apply ContinuousLinearMap.le_opNorm norm_nonneg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero MulOpposite.op_injective SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul map_mul NonUnitalAlgSemiHomClass.toMulHomClass NonUnitalAlgHom.instNonUnitalAlgSemiHomClass Real.sqrt_sq Real.sqrt_mul Real.sqrt_monotone Real.sqrt_le_sqrt_iff Real.sqrt_mul_self
instCompleteSpace 📖	mathematical	—	CompleteSpace CStarMatrix instUniformSpace	—	Pi.complete NonUnitalCStarAlgebra.toCompleteSpace
instContinuousSMul 📖	mathematical	—	ContinuousSMul CStarMatrix instSMul instTopologicalSpace	—	instContinuousSMulForall
instFinite 📖	mathematical	—	Finite CStarMatrix	—	Pi.finite
instIsCentralScalar 📖	mathematical	—	IsCentralScalar CStarMatrix instSMul MulOpposite	—	Pi.isCentralScalar
instIsScalarTower 📖	mathematical	—	IsScalarTower CStarMatrix instSMul	—	Pi.isScalarTower
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup CStarMatrix instTopologicalSpace instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing	—	Pi.topologicalAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup CStarMatrix instUniformSpace instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing	—	Pi.instIsUniformAddGroup SeminormedAddCommGroup.to_isUniformAddGroup
instNontrivial 📖	mathematical	—	Nontrivial CStarMatrix	—	Function.nontrivial
instSMulCommClass 📖	mathematical	—	SMulCommClass CStarMatrix instSMul	—	Pi.smulCommClass Function.smulCommClass
instStarModule 📖	mathematical	—	StarModule CStarMatrix instStar instSMul	—	Matrix.instStarModule
instStarOrderedRing 📖	mathematical	—	StarOrderedRing CStarMatrix instNonUnitalSemiring NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing instPartialOrder instStarRing NonUnitalCStarAlgebra.toStarRing	—	CStarAlgebra.spectralOrderedRing
instSubsingleton 📖	mathematical	—	CStarMatrix	—	—
instT2Space 📖	mathematical	—	T2Space CStarMatrix instTopologicalSpace	—	Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
instT3Space 📖	mathematical	—	T3Space CStarMatrix instTopologicalSpace	—	instT3Space T1Space.t0Space T2Space.t1Space instT2Space UniformSpace.to_regularSpace
map_apply 📖	mathematical	—	map	—	—
map_id 📖	mathematical	—	map	—	ext
map_id' 📖	mathematical	—	map	—	map_id
map_injective 📖	mathematical	—	CStarMatrix map	—	ext ext_iff
map_map 📖	mathematical	—	Matrix.map	—	Matrix.ext
mapₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap CStarMatrix instAddCommMonoid instModule LinearMap.instFunLike mapₗ map	—	—
mapₗ_reindexₐ 📖	mathematical	—	DFunLike.coe StarAlgEquiv CStarMatrix instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instMulOfFintypeOfAddCommMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instStar StarAlgEquiv.instFunLike reindexₐ LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule LinearMap.instFunLike mapₗ	—	—
mapₙₐ_apply 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom CStarMatrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero instNonUnitalNonAssocSemiring instDistribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction instStar NonUnitalStarAlgHom.instFunLike mapₙₐ LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule LinearMap.instFunLike mapₗ SemilinearMapClass.semilinearMap	—	—
mul_add 📖	mathematical	—	CStarMatrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid instAdd Distrib.toAdd	—	Matrix.mul_add
mul_apply 📖	mathematical	—	CStarMatrix instHMulOfFintypeOfMulOfAddCommMonoid Finset.sum Finset.univ	—	—
mul_apply' 📖	mathematical	—	CStarMatrix instHMulOfFintypeOfMulOfAddCommMonoid dotProduct	—	—
mul_entry_mul_eq_inner_toCLM 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing Inner.inner WithCStarModule CStarModule.toInner NonUnitalRing.toNonUnitalSemiring NormedSpace.toModule Complex Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNormedSpace WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup WithCStarModule.instModule Complex.instSemiring Pi.module ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instSMul Pi.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNormedRing.toNorm WithCStarModule.instNormForall WithCStarModule.instCStarModule WithCStarModule.instCStarModuleForall DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm WithCStarModule.equiv Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring WithCStarModule.instUniformSpace Pi.uniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace WithCStarModule.instNormedAddCommGroupForall AddCommGroup.toAddCommMonoid Pi.Function.module ContinuousLinearMap.funLike LinearMap CStarMatrix instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM	—	WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mul_assoc toCLM_apply_single WithCStarModule.inner_single_left
mul_smul 📖	mathematical	—	CStarMatrix instHMulOfFintypeOfMulOfAddCommMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Matrix.mul_smul
mul_zero 📖	mathematical	—	CStarMatrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.mul_zero
neg_apply 📖	mathematical	—	CStarMatrix instNeg	—	—
neg_of 📖	mathematical	—	CStarMatrix instNeg DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike ofMatrix Matrix.neg	—	—
norm_def 📖	mathematical	—	Norm.norm CStarMatrix instNorm ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring WithCStarModule UniformSpace.toTopologicalSpace WithCStarModule.instUniformSpace Pi.uniformSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instNormedAddCommGroupForall NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing WithCStarModule.instCStarModule AddCommGroup.toAddCommMonoid WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithCStarModule.instModule Pi.Function.module ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField WithCStarModule.instNormedSpaceComplexForall DFunLike.coe LinearMap instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM	—	—
norm_def' 📖	mathematical	—	Norm.norm CStarMatrix instNorm MulOpposite ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring WithCStarModule UniformSpace.toTopologicalSpace WithCStarModule.instUniformSpace Pi.uniformSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instNormedAddCommGroupForall NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing WithCStarModule.instCStarModule WithCStarModule.instModule Pi.addCommGroup NormedAddCommGroup.toAddCommGroup Pi.Function.module NormedRing.toNorm MulOpposite.instNormedRing ContinuousLinearMap.toNormedRing DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField WithCStarModule.instNormedSpaceComplexForall DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonUnitalNonAssocSemiring instDistribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction MulOpposite.instNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.ring Complex.instRing WithCStarModule.instAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MulOpposite.instDistribMulAction ContinuousLinearMap.distribMulAction UniformContinuousConstSMul.to_continuousConstSMul DistribMulAction.toDistribSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex Complex.instZero WithCStarModule.instZero Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul WithCStarModule.instSMulCommClass Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing NonUnitalAlgHom.instFunLike_1 toCLMNonUnitalAlgHom	—	—
norm_entry_le_norm 📖	mathematical	—	Real Real.instLE Norm.norm NonUnitalNormedRing.toNorm NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarMatrix instNorm	—	CStarRing.norm_star_mul_self NonUnitalCStarAlgebra.toCStarRing WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul toCLM_apply_single_apply LE.le.trans WithCStarModule.norm_apply_le_norm ContinuousLinearMap.le_opNorm RingHomIsometric.ids WithCStarModule.norm_single norm_star CStarRing.to_normedStarGroup eq_zero_or_norm_pos norm_zero le_of_mul_le_mul_right RCLike.instMulPosReflectLE
norm_le_of_forall_inner_le 📖	mathematical	Real Real.instLE Norm.norm NonUnitalNormedRing.toNorm NonUnitalCStarAlgebra.toNonUnitalNormedRing Inner.inner WithCStarModule CStarModule.toInner NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toStarRing NormedSpace.toModule Complex Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNormedSpace WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup WithCStarModule.instModule Complex.instSemiring Pi.module ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instSMul Pi.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing WithCStarModule.instNormForall WithCStarModule.instCStarModule WithCStarModule.instCStarModuleForall DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring WithCStarModule.instUniformSpace Pi.uniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace WithCStarModule.instNormedAddCommGroupForall AddCommGroup.toAddCommMonoid Pi.Function.module ContinuousLinearMap.funLike LinearMap CStarMatrix instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM Real.instMul NNReal.toReal	instNorm	—	WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.opNorm_le_bound LE.le.eq_or_lt norm_nonneg mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg le_of_mul_le_mul_right RCLike.instMulPosReflectLE CStarModule.norm_sq_eq
normedSpaceCore 📖	mathematical	—	NormedSpace.Core Complex CStarMatrix Complex.instNormedField instAddCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace instNorm	—	ContinuousLinearMap.opNorm_nonneg WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul norm_def UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass norm_smul NormedSpace.toNormSMulClass RingHomIsometric.ids SemilinearMapClass.toAddHomClass norm_add_le DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass toCLM_injective
ofMatrix_apply 📖	mathematical	—	DFunLike.coe Equiv Matrix CStarMatrix EquivLike.toFunLike Equiv.instEquivLike ofMatrix	—	—
ofMatrix_eq_ofMatrixL 📖	mathematical	—	DFunLike.coe Equiv Matrix CStarMatrix EquivLike.toFunLike Equiv.instEquivLike ofMatrix ContinuousLinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceMatrix UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing Matrix.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup instTopologicalSpace instAddCommMonoid Matrix.module NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace instModule ContinuousLinearEquiv.equivLike ofMatrixL	—	—
ofMatrix_eq_ofMatrixStarAlgEquiv 📖	mathematical	—	DFunLike.coe Equiv Matrix CStarMatrix EquivLike.toFunLike Equiv.instEquivLike ofMatrix StarAlgEquiv Complex Matrix.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instAdd Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toAddCommMonoid instMulOfFintypeOfAddCommMonoid Matrix.smul instSMul Matrix.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid instStar StarAlgEquiv.instFunLike ofMatrixStarAlgEquiv	—	—
ofMatrix_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CStarMatrix Matrix EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofMatrix	—	—
of_add_of 📖	mathematical	—	CStarMatrix instAdd DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike ofMatrix Matrix.add	—	—
of_sub_of 📖	mathematical	—	CStarMatrix instSub DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike ofMatrix Matrix.sub	—	—
of_zero 📖	mathematical	—	DFunLike.coe Equiv Matrix CStarMatrix EquivLike.toFunLike Equiv.instEquivLike ofMatrix Matrix.zero instZero	—	—
one_apply 📖	mathematical	—	CStarMatrix instOne	—	—
one_apply_eq 📖	mathematical	—	CStarMatrix instOne	—	Matrix.one_apply_eq
one_apply_ne 📖	mathematical	—	CStarMatrix instOne	—	Matrix.one_apply_ne
one_apply_ne' 📖	mathematical	—	CStarMatrix instOne	—	Matrix.one_apply_ne'
reindexₐ_apply 📖	mathematical	—	DFunLike.coe StarAlgEquiv CStarMatrix instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instMulOfFintypeOfAddCommMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instStar StarAlgEquiv.instFunLike reindexₐ Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex	—	—
reindexₐ_symm 📖	mathematical	—	reindexₐ Equiv.symm StarAlgEquiv.symm CStarMatrix instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instMulOfFintypeOfAddCommMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instStar	—	RingHomInvPair.ids
reindexₗ_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CStarMatrix instAddCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reindexₗ Equiv Matrix Equiv.instEquivLike Matrix.reindex	—	RingHomInvPair.ids
smul_apply 📖	mathematical	—	CStarMatrix instSMul	—	—
smul_mul 📖	mathematical	—	CStarMatrix instHMulOfFintypeOfMulOfAddCommMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Matrix.smul_mul
smul_of 📖	mathematical	—	CStarMatrix instSMul DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike ofMatrix Matrix.smul	—	—
star_apply 📖	mathematical	—	Star.star CStarMatrix instStar	—	star_eq_conjTranspose conjTranspose_apply
star_apply_of_isSelfAdjoint 📖	mathematical	IsSelfAdjoint CStarMatrix instStar	Star.star	—	star_apply IsSelfAdjoint.star_eq
star_eq_conjTranspose 📖	mathematical	—	Star.star CStarMatrix instStar conjTranspose	—	—
sub_apply 📖	mathematical	—	CStarMatrix instSub	—	—
toCLMNonUnitalAlgHom_eq_toCLM 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CStarMatrix MulOpposite ContinuousLinearMap RingHom.id WithCStarModule UniformSpace.toTopologicalSpace WithCStarModule.instUniformSpace Pi.uniformSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instNormedAddCommGroupForall NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing WithCStarModule.instCStarModule WithCStarModule.instModule Pi.addCommGroup NormedAddCommGroup.toAddCommGroup Pi.Function.module instNonUnitalNonAssocSemiring instDistribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction MulOpposite.instNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.ring Complex.instRing WithCStarModule.instAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MulOpposite.instDistribMulAction ContinuousLinearMap.distribMulAction UniformContinuousConstSMul.to_continuousConstSMul DistribMulAction.toDistribSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex Complex.instZero WithCStarModule.instZero Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul WithCStarModule.instNormedSpaceComplexForall WithCStarModule.instSMulCommClass Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing NonUnitalAlgHom.instFunLike_1 toCLMNonUnitalAlgHom MulOpposite.op AddCommGroup.toAddCommMonoid LinearMap instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul LinearMap.instFunLike toCLM	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self
toCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring WithCStarModule UniformSpace.toTopologicalSpace WithCStarModule.instUniformSpace Pi.uniformSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instNormedAddCommGroupForall NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing WithCStarModule.instCStarModule AddCommGroup.toAddCommMonoid WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithCStarModule.instModule Pi.Function.module ContinuousLinearMap.funLike LinearMap CStarMatrix instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm WithCStarModule.equiv Matrix.vecMul	—	WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
toCLM_apply_eq_sum 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring WithCStarModule UniformSpace.toTopologicalSpace WithCStarModule.instUniformSpace Pi.uniformSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instNormedAddCommGroupForall NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing WithCStarModule.instCStarModule AddCommGroup.toAddCommMonoid WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithCStarModule.instModule Pi.Function.module ContinuousLinearMap.funLike LinearMap CStarMatrix instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm WithCStarModule.equiv Finset.sum Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	WithCStarModule.ext WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Finset.sum_congr
toCLM_apply_single 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring WithCStarModule UniformSpace.toTopologicalSpace WithCStarModule.instUniformSpace Pi.uniformSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instNormedAddCommGroupForall NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing WithCStarModule.instCStarModule AddCommGroup.toAddCommMonoid WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithCStarModule.instModule Pi.Function.module ContinuousLinearMap.funLike LinearMap CStarMatrix instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm WithCStarModule.equiv Pi.single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	WithCStarModule.ext WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Matrix.single_vecMul
toCLM_apply_single_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring WithCStarModule UniformSpace.toTopologicalSpace WithCStarModule.instUniformSpace Pi.uniformSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instNormedAddCommGroupForall NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing WithCStarModule.instCStarModule AddCommGroup.toAddCommMonoid WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithCStarModule.instModule Pi.Function.module ContinuousLinearMap.funLike LinearMap CStarMatrix instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm WithCStarModule.equiv Pi.single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul toCLM_apply_single
toCLM_injective 📖	mathematical	—	CStarMatrix ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring WithCStarModule UniformSpace.toTopologicalSpace WithCStarModule.instUniformSpace Pi.uniformSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithCStarModule.instNormedAddCommGroupForall NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing WithCStarModule.instCStarModule AddCommGroup.toAddCommMonoid WithCStarModule.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithCStarModule.instModule Pi.Function.module DFunLike.coe LinearMap instAddCommMonoid ContinuousLinearMap.addCommMonoid WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instModule ContinuousLinearMap.module WithCStarModule.instSMulCommClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction smulCommClass_self CommRing.toCommMonoid Complex.commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NormedSpace.toIsBoundedSMul LinearMap.instFunLike toCLM	—	WithCStarModule.instContinuousAdd instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing WithCStarModule.instSMulCommClass Function.smulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul WithCStarModule.instContinuousSMul instContinuousSMulForall IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsUniformAddGroup.to_topologicalAddGroup WithCStarModule.instIsUniformAddGroup Pi.instIsUniformAddGroup SeminormedAddCommGroup.to_isUniformAddGroup injective_iff_map_eq_zero DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass ext Matrix.zero_apply norm_eq_zero sq_eq_zero_iff isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass sq CStarRing.norm_star_mul_self NonUnitalCStarAlgebra.toCStarRing toCLM_apply_single_apply norm_zero
transpose_apply 📖	mathematical	—	transpose	—	—
uniformEmbedding_ofMatrix 📖	mathematical	—	IsUniformEmbedding Matrix CStarMatrix Matrix.instUniformSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing instUniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofMatrix	—	Filter.comap_id'
zero_apply 📖	mathematical	—	CStarMatrix instZero	—	—
zero_mul 📖	mathematical	—	CStarMatrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.zero_mul

(root)

Definitions

Name	Category	Theorems
CStarMatrix 📖	CompOp	66 math math: CStarMatrix.norm_entry_le_norm, CStarMatrix.mapₗ_reindexₐ, CStarMatrix.mul_smul, CStarMatrix.instIsUniformAddGroup, CStarMatrix.ofMatrix_apply, CStarMatrix.toCLM_injective, CStarMatrix.instStarOrderedRing, CStarMatrix.zero_mul, CStarMatrix.norm_def', CStarMatrix.instNontrivial, CStarMatrix.inner_toCLM_conjTranspose_left, CStarMatrix.zero_apply, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, CStarMatrix.mul_add, CStarMatrix.sub_apply, CStarMatrix.instContinuousSMul, CStarMatrix.mul_apply, CStarMatrix.algebraMap_apply, CStarMatrix.instFinite, CStarMatrix.of_sub_of, CStarMatrix.instCompleteSpace, CStarMatrix.star_apply, CStarMatrix.one_apply, CStarMatrix.toCLM_apply_single, CStarMatrix.instSubsingleton, CStarMatrix.toCLM_apply_eq_sum, CStarMatrix.one_apply_ne, CStarMatrix.one_apply_ne', CStarMatrix.reindexₐ_apply, CStarMatrix.ofMatrix_eq_ofMatrixL, CStarMatrix.instIsTopologicalAddGroup, CStarMatrix.toCLM_apply, CStarMatrix.smul_of, CStarMatrix.add_apply, CStarMatrix.mul_zero, CStarMatrix.mul_entry_mul_eq_inner_toCLM, CStarMatrix.ofMatrix_symm_apply, CStarMatrix.instT2Space, CStarMatrix.instIsCentralScalar, CStarMatrix.smul_mul, CStarMatrix.reindexₐ_symm, CStarMatrix.reindexₗ_apply, CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv, CStarMatrix.one_apply_eq, CStarMatrix.normedSpaceCore, CStarMatrix.instSMulCommClass, CStarMatrix.conjTranspose_zero, CStarMatrix.map_injective, CStarMatrix.neg_of, CStarMatrix.neg_apply, CStarMatrix.star_eq_conjTranspose, CStarMatrix.instT3Space, CStarMatrix.smul_apply, CStarMatrix.uniformEmbedding_ofMatrix, CStarMatrix.instStarModule, CStarMatrix.instCStarRing, CStarMatrix.of_zero, CStarMatrix.of_add_of, CStarMatrix.mul_apply', CStarMatrix.mapₙₐ_apply, CStarMatrix.add_mul, CStarMatrix.mapₗ_apply, CStarMatrix.norm_def, CStarMatrix.inner_toCLM_conjTranspose_right, CStarMatrix.toCLM_apply_single_apply, CStarMatrix.instIsScalarTower

---

← Back to Index