Synonym

📁 Source: Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean

Statistics

Metric	Count
Definitions `WithCStarModule`, `addEquiv`, `equiv`, `equivL`, `instAdd`, `instAddCommGroup`, `instAddMonoid`, `instBornology`, `instCoeFunForall`, `instInhabited`, `instModule`, `instNeg`, `instSMul`, `instSub`, `instSubNegMonoid`, `instSubNegZeroMonoid`, `instUniformSpace`, `instUnique`, `instZero`, `linearEquiv`, `uniformEquiv`, `«termC⋆ᵐᵒᵈ(_,_)»`»)	22
Theorems `add_apply`, `add_fst`, `add_snd`, `equivL_apply`, `equivL_symm_apply`, `equiv_add`, `equiv_fst`, `equiv_neg`, `equiv_pi_apply`, `equiv_smul`, `equiv_snd`, `equiv_sub`, `equiv_symm_add`, `equiv_symm_fst`, `equiv_symm_neg`, `equiv_symm_pi_apply`, `equiv_symm_smul`, `equiv_symm_snd`, `equiv_symm_sub`, `equiv_symm_zero`, `equiv_zero`, `ext`, `ext_iff`, `instCompleteSpace`, `instContinuousAdd`, `instContinuousSMul`, `instIsScalarTower`, `instIsUniformAddGroup`, `instModuleFinite`, `instNonempty`, `instNontrivial`, `instSMulCommClass`, `linearEquiv_apply`, `linearEquiv_symm_apply`, `map_top_submodule`, `neg_apply`, `neg_fst`, `neg_snd`, `smul_apply`, `smul_fst`, `smul_snd`, `sub_apply`, `sub_fst`, `sub_snd`, `zero_apply`, `zero_fst`, `zero_snd`	47
Total	69

WithCStarModule

Definitions

Name	Category	Theorems
`addEquiv` 📖	CompOp	—
`equiv` 📖	CompOp	30 math math: `equiv_add`, `equiv_symm_snd`, `equiv_symm_neg`, `equiv_neg`, `equiv_symm_smul`, `linearEquiv_apply`, `CStarMatrix.toCLM_apply_single`, `equiv_zero`, `CStarMatrix.toCLM_apply_eq_sum`, `CStarMatrix.toCLM_apply`, `linearEquiv_symm_apply`, `norm_single`, `equiv_symm_sub`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `inner_single_right`, `equiv_smul`, `norm_equiv_le_norm_prod`, `equiv_pi_apply`, `equiv_sub`, `equiv_snd`, `norm_equiv_le_norm_pi`, `inner_single_left`, `equiv_symm_add`, `equiv_fst`, `equiv_symm_fst`, `equivL_symm_apply`, `equiv_symm_pi_apply`, `equivL_apply`, `equiv_symm_zero`, `CStarMatrix.toCLM_apply_single_apply`
`equivL` 📖	CompOp	2 math math: `equivL_symm_apply`, `equivL_apply`
`instAdd` 📖	CompOp	6 math math: `add_fst`, `equiv_add`, `add_apply`, `instContinuousAdd`, `equiv_symm_add`, `add_snd`
`instAddCommGroup` 📖	CompOp	22 math math: `instIsUniformAddGroup`, `CStarMatrix.toCLM_injective`, `CStarMatrix.norm_def'`, `CStarMatrix.inner_toCLM_conjTranspose_left`, `CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM`, `linearEquiv_apply`, `CStarMatrix.toCLM_apply_single`, `CStarMatrix.toCLM_apply_eq_sum`, `CStarMatrix.toCLM_apply`, `linearEquiv_symm_apply`, `pi_inner`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `inner_single_right`, `map_top_submodule`, `inner_single_left`, `equivL_symm_apply`, `equivL_apply`, `prod_inner`, `instModuleFinite`, `CStarMatrix.norm_def`, `CStarMatrix.inner_toCLM_conjTranspose_right`, `CStarMatrix.toCLM_apply_single_apply`
`instAddMonoid` 📖	CompOp	—
`instBornology` 📖	CompOp	—
`instCoeFunForall` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	21 math math: `CStarMatrix.toCLM_injective`, `CStarMatrix.norm_def'`, `CStarMatrix.inner_toCLM_conjTranspose_left`, `CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM`, `linearEquiv_apply`, `CStarMatrix.toCLM_apply_single`, `CStarMatrix.toCLM_apply_eq_sum`, `CStarMatrix.toCLM_apply`, `linearEquiv_symm_apply`, `pi_inner`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `inner_single_right`, `map_top_submodule`, `inner_single_left`, `equivL_symm_apply`, `equivL_apply`, `prod_inner`, `instModuleFinite`, `CStarMatrix.norm_def`, `CStarMatrix.inner_toCLM_conjTranspose_right`, `CStarMatrix.toCLM_apply_single_apply`
`instNeg` 📖	CompOp	5 math math: `neg_fst`, `neg_snd`, `equiv_symm_neg`, `equiv_neg`, `neg_apply`
`instSMul` 📖	CompOp	15 math math: `smul_fst`, `CStarMatrix.inner_toCLM_conjTranspose_left`, `equiv_symm_smul`, `pi_inner`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `inner_single_right`, `equiv_smul`, `instContinuousSMul`, `inner_single_left`, `instIsScalarTower`, `instSMulCommClass`, `smul_snd`, `smul_apply`, `prod_inner`, `CStarMatrix.inner_toCLM_conjTranspose_right`
`instSub` 📖	CompOp	5 math math: `sub_snd`, `equiv_symm_sub`, `equiv_sub`, `sub_apply`, `sub_fst`
`instSubNegMonoid` 📖	CompOp	—
`instSubNegZeroMonoid` 📖	CompOp	—
`instUniformSpace` 📖	CompOp	17 math math: `instIsUniformAddGroup`, `CStarMatrix.toCLM_injective`, `CStarMatrix.norm_def'`, `CStarMatrix.inner_toCLM_conjTranspose_left`, `CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM`, `instCompleteSpace`, `CStarMatrix.toCLM_apply_single`, `CStarMatrix.toCLM_apply_eq_sum`, `CStarMatrix.toCLM_apply`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `instContinuousSMul`, `instContinuousAdd`, `equivL_symm_apply`, `equivL_apply`, `CStarMatrix.norm_def`, `CStarMatrix.inner_toCLM_conjTranspose_right`, `CStarMatrix.toCLM_apply_single_apply`
`instUnique` 📖	CompOp	—
`instZero` 📖	CompOp	7 math math: `CStarMatrix.norm_def'`, `zero_apply`, `CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM`, `equiv_zero`, `zero_snd`, `zero_fst`, `equiv_symm_zero`
`linearEquiv` 📖	CompOp	3 math math: `linearEquiv_apply`, `linearEquiv_symm_apply`, `map_top_submodule`
`uniformEquiv` 📖	CompOp	—
`«termC⋆ᵐᵒᵈ(_,_)»` 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`WithCStarModule` `instAdd` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`add_fst` 📖	mathematical	—	`WithCStarModule` `instAdd` `Prod.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`add_snd` 📖	mathematical	—	`WithCStarModule` `instAdd` `Prod.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`equivL_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithCStarModule` `UniformSpace.toTopologicalSpace` `instUniformSpace` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equivL` `Equiv` `Equiv.instEquivLike` `equiv`	—	`RingHomInvPair.ids`
`equivL_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `AddCommGroup.toAddCommMonoid` `WithCStarModule` `instUniformSpace` `instAddCommGroup` `instModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `equivL` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `equiv`	—	`RingHomInvPair.ids`
`equiv_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`equiv_fst` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	—
`equiv_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`equiv_pi_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	—
`equiv_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `instSMul`	—	—
`equiv_snd` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	—
`equiv_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`equiv_symm_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `instAdd`	—	—
`equiv_symm_fst` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv`	—	—
`equiv_symm_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instNeg`	—	—
`equiv_symm_pi_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv`	—	—
`equiv_symm_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `instSMul`	—	—
`equiv_symm_snd` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv`	—	—
`equiv_symm_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instSub`	—	—
`equiv_symm_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instZero`	—	—
`equiv_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `WithCStarModule` `instUniformSpace`	—	`UniformEquiv.completeSpace_iff`
`instContinuousAdd` 📖	mathematical	—	`ContinuousAdd` `WithCStarModule` `UniformSpace.toTopologicalSpace` `instUniformSpace` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`ContinuousAdd.induced` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`instContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `WithCStarModule` `instSMul` `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` `UniformSpace.toTopologicalSpace` `instUniformSpace`	—	`ContinuousSMul.induced` `RingHomInvPair.ids` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `WithCStarModule` `instSMul`	—	—
`instIsUniformAddGroup` 📖	mathematical	—	`IsUniformAddGroup` `WithCStarModule` `instUniformSpace` `AddCommGroup.toAddGroup` `instAddCommGroup`	—	`IsUniformAddGroup.comap` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`instModuleFinite` 📖	mathematical	—	`Module.Finite` `WithCStarModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModule`	—	—
`instNonempty` 📖	mathematical	—	`WithCStarModule`	—	—
`instNontrivial` 📖	mathematical	—	`Nontrivial` `WithCStarModule`	—	—
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `WithCStarModule` `instSMul`	—	—
`linearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithCStarModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `linearEquiv` `Equiv` `Equiv.instEquivLike` `equiv`	—	`RingHomInvPair.ids`
`linearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithCStarModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `linearEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `equiv`	—	`RingHomInvPair.ids`
`map_top_submodule` 📖	mathematical	—	`Submodule.map` `WithCStarModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `linearEquiv` `Top.top` `Submodule` `Submodule.instTop`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `Submodule.map_eq_top_iff`
`neg_apply` 📖	mathematical	—	`WithCStarModule` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`neg_fst` 📖	mathematical	—	`WithCStarModule` `instNeg` `Prod.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`neg_snd` 📖	mathematical	—	`WithCStarModule` `instNeg` `Prod.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`smul_apply` 📖	mathematical	—	`WithCStarModule` `instSMul` `Pi.instSMul`	—	—
`smul_fst` 📖	mathematical	—	`WithCStarModule` `instSMul` `Prod.instSMul`	—	—
`smul_snd` 📖	mathematical	—	`WithCStarModule` `instSMul` `Prod.instSMul`	—	—
`sub_apply` 📖	mathematical	—	`WithCStarModule` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`sub_fst` 📖	mathematical	—	`WithCStarModule` `instSub` `Prod.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`sub_snd` 📖	mathematical	—	`WithCStarModule` `instSub` `Prod.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`zero_apply` 📖	mathematical	—	`WithCStarModule` `instZero` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`zero_fst` 📖	mathematical	—	`WithCStarModule` `instZero` `Prod.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`zero_snd` 📖	mathematical	—	`WithCStarModule` `instZero` `Prod.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—

(root)

Definitions

Name	Category	Theorems
`WithCStarModule` 📖	CompOp	71 math math: `WithCStarModule.add_fst`, `WithCStarModule.equiv_add`, `WithCStarModule.neg_fst`, `WithCStarModule.add_apply`, `WithCStarModule.neg_snd`, `WithCStarModule.instIsUniformAddGroup`, `WithCStarModule.equiv_symm_snd`, `WithCStarModule.prod_norm_sq`, `CStarMatrix.toCLM_injective`, `WithCStarModule.smul_fst`, `CStarMatrix.norm_def'`, `WithCStarModule.equiv_symm_neg`, `CStarMatrix.inner_toCLM_conjTranspose_left`, `WithCStarModule.zero_apply`, `CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM`, `WithCStarModule.prod_norm_le_norm_add`, `WithCStarModule.norm_apply_le_norm`, `WithCStarModule.equiv_neg`, `WithCStarModule.neg_apply`, `WithCStarModule.instCompleteSpace`, `WithCStarModule.sub_snd`, `WithCStarModule.equiv_symm_smul`, `WithCStarModule.linearEquiv_apply`, `CStarMatrix.toCLM_apply_single`, `WithCStarModule.equiv_zero`, `WithCStarModule.zero_snd`, `CStarMatrix.toCLM_apply_eq_sum`, `WithCStarModule.pi_norm`, `CStarMatrix.toCLM_apply`, `WithCStarModule.linearEquiv_symm_apply`, `WithCStarModule.pi_inner`, `WithCStarModule.norm_single`, `WithCStarModule.prod_norm`, `WithCStarModule.equiv_symm_sub`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `WithCStarModule.inner_single_right`, `WithCStarModule.equiv_smul`, `WithCStarModule.instContinuousSMul`, `WithCStarModule.instContinuousAdd`, `WithCStarModule.norm_equiv_le_norm_prod`, `WithCStarModule.map_top_submodule`, `WithCStarModule.pi_norm_le_sum_norm`, `WithCStarModule.equiv_pi_apply`, `WithCStarModule.equiv_sub`, `WithCStarModule.equiv_snd`, `WithCStarModule.norm_equiv_le_norm_pi`, `WithCStarModule.inner_single_left`, `WithCStarModule.instIsScalarTower`, `WithCStarModule.zero_fst`, `WithCStarModule.equiv_symm_add`, `WithCStarModule.instNontrivial`, `WithCStarModule.equiv_fst`, `WithCStarModule.add_snd`, `WithCStarModule.sub_apply`, `WithCStarModule.pi_norm_sq`, `WithCStarModule.equiv_symm_fst`, `WithCStarModule.max_le_prod_norm`, `WithCStarModule.equivL_symm_apply`, `WithCStarModule.sub_fst`, `WithCStarModule.instSMulCommClass`, `WithCStarModule.equiv_symm_pi_apply`, `WithCStarModule.smul_snd`, `WithCStarModule.equivL_apply`, `WithCStarModule.smul_apply`, `WithCStarModule.prod_inner`, `WithCStarModule.instModuleFinite`, `WithCStarModule.equiv_symm_zero`, `CStarMatrix.norm_def`, `WithCStarModule.instNonempty`, `CStarMatrix.inner_toCLM_conjTranspose_right`, `CStarMatrix.toCLM_apply_single_apply`

---

← Back to Index