Defs

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

Statistics

Metric	Count
Definitions `CStarModule`, `innerSL`, `innerₛₗ`, `norm`, `normedAddCommGroup`, `toInner`	6
Theorems `continuous_inner`, `innerSL_apply`, `inner_add_left`, `inner_add_right`, `inner_mul_inner_swap_le`, `inner_neg_left`, `inner_neg_right`, `inner_op_smul_left`, `inner_op_smul_right`, `inner_self`, `inner_self_nonneg`, `inner_smul_left_complex`, `inner_smul_left_real`, `inner_smul_right_complex`, `inner_smul_right_real`, `inner_sub_left`, `inner_sub_right`, `inner_sum_left`, `inner_sum_right`, `inner_zero_left`, `inner_zero_right`, `innerₛₗ_apply`, `isSelfAdjoint_inner_self`, `norm_eq_csSup`, `norm_eq_sqrt_norm_inner_self`, `norm_inner_le`, `norm_nonneg`, `norm_pos`, `norm_sq_eq`, `norm_triangle`, `norm_zero`, `norm_zero_iff`, `normedSpaceCore`, `star_inner`	34
Total	40

CStarModule

Definitions

Name	Category	Theorems
`innerSL` 📖	CompOp	1 math math: `innerSL_apply`
`innerₛₗ` 📖	CompOp	1 math math: `innerₛₗ_apply`
`norm` 📖	CompOp	—
`normedAddCommGroup` 📖	CompOp	—
`toInner` 📖	CompOp	40 math math: `innerₛₗ_apply`, `inner_sub_left`, `WithCStarModule.prod_norm_sq`, `innerSL_apply`, `WithCStarModule.inner_def`, `CStarMatrix.inner_toCLM_conjTranspose_left`, `inner_smul_right_real`, `inner_smul_right_complex`, `inner_smul_left_complex`, `star_inner`, `norm_eq_sqrt_norm_inner_self`, `norm_inner_le`, `inner_self`, `inner_zero_left`, `WithCStarModule.pi_norm`, `inner_zero_right`, `inner_sub_right`, `WithCStarModule.pi_inner`, `WithCStarModule.prod_norm`, `inner_op_smul_left`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `norm_sq_eq`, `WithCStarModule.inner_single_right`, `inner_smul_left_real`, `norm_eq_csSup`, `inner_neg_right`, `inner_op_smul_right`, `inner_add_left`, `inner_mul_inner_swap_le`, `WithCStarModule.inner_single_left`, `inner_sum_left`, `inner_add_right`, `inner_self_nonneg`, `continuous_inner`, `inner_sum_right`, `WithCStarModule.pi_norm_sq`, `inner_neg_left`, `WithCStarModule.prod_inner`, `isSelfAdjoint_inner_self`, `CStarMatrix.inner_toCLM_conjTranspose_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_inner` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNorm` `NormedAddCommGroup.toNorm`	—	`Continuous.clm_apply` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Continuous.comp'` `ContinuousLinearMap.continuous` `Continuous.fst` `continuous_id'` `Continuous.snd`
`innerSL_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `ContinuousLinearMap.funLike` `CommSemiring.toSemiring` `Complex.instCommSemiring` `starRingEnd` `Complex.instStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Complex.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NormedSpace.toIsBoundedSMul` `innerSL` `Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalCStarAlgebra.toStarRing` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNorm` `NormedAddCommGroup.toNorm`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`inner_add_left` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`star_star` `star_inner` `inner_add_right` `StarAddMonoid.star_add`
`inner_add_right` 📖	mathematical	—	`Inner.inner` `toInner` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	—
`inner_mul_inner_swap_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `NonUnitalNormedRing.toNorm` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NonUnitalSeminormedRing.toPseudoMetricSpace` `Real.normedField` `NormedSpace.complexToReal` `Monoid.toNatPow` `Norm.norm`	—	`eq_or_ne` `inner_zero_left` `NonUnitalCStarAlgebra.toStarModule` `inner_zero_right` `MulZeroClass.mul_zero` `norm_zero` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `zero_smul` `inner_self_nonneg` `inner_sub_right` `inner_op_smul_right` `inner_sub_left` `inner_op_smul_left` `inner_smul_left_real` `mul_sub` `mul_smul_comm` `SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `inner_smul_right_real` `smul_sub` `mul_assoc` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `sub_le_sub_right` `CStarAlgebra.star_right_conjugate_le_norm_smul` `Real.sq_sqrt` `norm_nonneg` `norm_eq_sqrt_norm_inner_self` `smul_le_smul_iff_of_pos_left` `IsOrderedModule.toPosSMulMono` `instIsOrderedModule` `Real.instStarOrderedRing` `StarModule.complexToReal` `IsScalarTower.complexToReal` `NonUnitalCStarAlgebra.toIsScalarTower` `PosSMulReflectLT.toPosSMulReflectLE` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `PosSMulStrictMono.toPosSMulReflectLT` `Real.instIsStrictOrderedRing` `instPosSMulStrictMono` `IsOrderedCancelAddMonoid.toIsCancelAdd` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instZeroLEOneClass` `norm_pos` `star_inner` `sub_self` `zero_sub` `add_zero`
`inner_neg_left` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`smulCommClass_self` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`inner_neg_right` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`smulCommClass_self` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`inner_op_smul_left` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`star_inner` `inner_op_smul_right` `StarMul.star_mul`
`inner_op_smul_right` 📖	mathematical	—	`Inner.inner` `toInner` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	—
`inner_self` 📖	mathematical	—	`Inner.inner` `toInner` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`inner_self_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Inner.inner` `toInner`	—	—
`inner_smul_left_complex` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `instCommCStarAlgebraComplex` `StarRing.toStarAddMonoid` `Complex.instStarRing`	—	`star_inner` `inner_smul_right_complex` `StarModule.star_smul`
`inner_smul_left_real` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `Module.complexToReal` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`star_inner` `inner_smul_right_complex` `StarModule.star_smul` `StarModule.complexToReal` `TrivialStar.star_trivial` `instTrivialStarReal`
`inner_smul_right_complex` 📖	mathematical	—	`Inner.inner` `toInner` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	—
`inner_smul_right_real` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `Module.complexToReal` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`star_inner` `inner_smul_left_complex` `Complex.conj_ofReal` `StarModule.star_smul` `StarModule.complexToReal` `TrivialStar.star_trivial` `instTrivialStarReal`
`inner_sub_left` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`smulCommClass_self` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`inner_sub_right` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`smulCommClass_self` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`inner_sum_left` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `Finset.sum` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `SMulCommClass.symm` `smulCommClass_self`
`inner_sum_right` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `Finset.sum` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smulCommClass_self`
`inner_zero_left` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`smulCommClass_self` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`inner_zero_right` 📖	mathematical	—	`Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smulCommClass_self`
`innerₛₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `LinearMap.instFunLike` `CommSemiring.toSemiring` `Complex.instCommSemiring` `starRingEnd` `Complex.instStarRing` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `innerₛₗ` `Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring`	—	`smulCommClass_self`
`isSelfAdjoint_inner_self` 📖	mathematical	—	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring`	—	`star_inner`
`norm_eq_csSup` 📖	mathematical	—	`Norm.norm` `SupSet.sSup` `Real` `Real.instSupSet` `setOf` `Real.instLE` `Real.instOne` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace`	—	`normedSpaceCore` `IsGreatest.csSup_eq` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_norm` `inv_mul_le_one_of_le₀` `RCLike.toPosMulReflectLT` `Real.instZeroLEOneClass` `le_rfl` `norm_nonneg` `inner_smul_left_real` `NonUnitalCStarAlgebra.toStarModule` `pow_two` `inv_mul_mul_self` `norm_inner_le` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `one_mul`
`norm_eq_sqrt_norm_inner_self` 📖	mathematical	—	`Norm.norm` `Real.sqrt` `Inner.inner` `toInner`	—	—
`norm_inner_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `Real.instMul`	—	`star_inner` `CStarRing.norm_self_mul_star` `NonUnitalCStarAlgebra.toCStarRing` `pow_two` `CStarAlgebra.norm_le_norm_of_nonneg_of_le` `mul_star_self_nonneg` `inner_mul_inner_swap_le` `norm_smul` `NormedSpace.toNormSMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `sq_abs` `norm_eq_sqrt_norm_inner_self` `Real.sq_sqrt` `mul_pow` `pow_le_pow_iff_left₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg` `mul_nonneg` `IsOrderedRing.toPosMulMono` `norm_nonneg` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`norm_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `Norm.norm`	—	`norm_eq_sqrt_norm_inner_self`
`norm_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Norm.norm`	—	`norm_eq_sqrt_norm_inner_self` `inner_self`
`norm_sq_eq` 📖	mathematical	—	`Real` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Inner.inner` `toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace`	—	`norm_eq_sqrt_norm_inner_self` `Real.sq_sqrt`
`norm_triangle` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Real.instAdd`	—	`norm_eq_sqrt_norm_inner_self` `inner_add_right` `inner_add_left` `Real.sq_sqrt` `norm_add₃_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `norm_add_le` `add_le_add` `add_le_add_right` `norm_inner_le` `Nat.instAtLeastTwoHAddOfNat` `add_pow_two` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `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_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_one` `pow_le_pow_iff_left₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg` `add_nonneg` `Nat.instCharZero`
`norm_zero` 📖	mathematical	—	`Norm.norm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real` `Real.instZero`	—	`norm_eq_sqrt_norm_inner_self` `inner_zero_right` `NonUnitalCStarAlgebra.toStarModule` `norm_zero` `Real.sqrt_zero`
`norm_zero_iff` 📖	mathematical	—	`Norm.norm` `Real` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`norm_eq_sqrt_norm_inner_self` `inner_zero_right` `NonUnitalCStarAlgebra.toStarModule` `norm_zero` `Real.sqrt_zero`
`normedSpaceCore` 📖	mathematical	—	`NormedSpace.Core` `Complex` `Complex.instNormedField`	—	`norm_nonneg` `norm_eq_sqrt_norm_inner_self` `inner_smul_right_complex` `inner_smul_left_complex` `NonUnitalCStarAlgebra.toStarModule` `norm_smul` `NormedSpace.toNormSMulClass` `RCLike.norm_conj` `Real.sqrt_mul'` `Real.sqrt_mul_self` `norm_triangle` `norm_zero_iff`
`star_inner` 📖	mathematical	—	`Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Inner.inner` `toInner`	—	—

(root)

Definitions

Name	Category	Theorems
`CStarModule` 📖	CompData	—

---

← Back to Index