Positive

📁 Source: Mathlib/Analysis/InnerProductSpace/Positive.lean

Statistics

Metric	Count
Definitions `IsPositive`, `instLoewnerPartialOrder`, `IsPositive`, `instLoewnerPartialOrder`	4
Theorems `isPositive_iff_isSelfAdjoint`, `add`, `adjoint_conj`, `conj_adjoint`, `conj_starProjection`, `inner_left_eq_inner_right`, `inner_nonneg_left`, `inner_nonneg_right`, `isSelfAdjoint`, `isSymmetric`, `of_isStarProjection`, `orthogonalProjection_comp`, `re_inner_nonneg_left`, `re_inner_nonneg_right`, `smul_of_nonneg`, `toLinearMap`, `antilipschitz_of_forall_le_inner_map`, `coe_le_coe_iff`, `isPositive_adjoint_comp_self`, `isPositive_def`, `isPositive_def'`, `isPositive_id`, `isPositive_iff`, `isPositive_iff'`, `isPositive_iff_complex`, `isPositive_iff_eq_sum_rankOne`, `isPositive_natCast`, `isPositive_ofNat`, `isPositive_one`, `isPositive_self_comp_adjoint`, `isPositive_sum`, `isPositive_toLinearMap_iff`, `isPositive_zero`, `isUnit_of_forall_le_norm_inner_map`, `le_def`, `nonneg_iff_isPositive`, `isPositive_rankOne_self`, `isPositive_symm_iff`, `isPositive_iff_isSymmetric`, `add`, `adjoint_conj`, `adjoint_eq`, `conj_adjoint`, `inner_nonneg_left`, `inner_nonneg_right`, `isPositive_smul_iff`, `isSelfAdjoint`, `isSymmetric`, `ne_zero_iff`, `nonneg_eigenvalues`, `of_isStarProjection`, `of_isSymmetricProjection`, `re_inner_nonneg_left`, `re_inner_nonneg_right`, `smul_of_nonneg`, `toLinearMap_symm`, `isPositive`, `le_iff_range_le_range`, `isPositive_adjoint_comp_self`, `isPositive_id`, `isPositive_iff`, `isPositive_iff_complex`, `isPositive_linearIsometryEquiv_conj_iff`, `isPositive_natCast`, `isPositive_ofNat`, `isPositive_one`, `isPositive_self_comp_adjoint`, `isPositive_sum`, `isPositive_toContinuousLinearMap_iff`, `isPositive_zero`, `le_def`, `nonneg_iff_isPositive`, `posSemidef_toMatrix_iff`, `isPositive_toEuclideanLin_iff`, `posSemidef_iff_eq_sum_vecMulVec`, `starProjection_inj`, `starProjection_le_starProjection_iff`	77
Total	81

ContinuousLinearMap

Definitions

Name	Category	Theorems
`IsPositive` 📖	MathDef	21 math math: `isPositive_iff_eq_sum_rankOne`, `InnerProductSpace.isPositive_rankOne_self`, `isPositive_natCast`, `IsPositive.of_isStarProjection`, `isPositive_self_comp_adjoint`, `isPositive_def`, `isPositive_id`, `isPositive_toLinearMap_iff`, `nonneg_iff_isPositive`, `IsIdempotentElem.TFAE`, `LinearMap.isPositive_toContinuousLinearMap_iff`, `le_def`, `IsIdempotentElem.isPositive_iff_isSelfAdjoint`, `isPositive_def'`, `isPositive_iff_complex`, `isPositive_iff`, `isPositive_iff'`, `isPositive_zero`, `isPositive_ofNat`, `isPositive_one`, `isPositive_adjoint_comp_self`
`instLoewnerPartialOrder` 📖	CompOp	8 math math: `instStarOrderedRing`, `nonneg_iff_isPositive`, `le_def`, `instNonnegSpectrumClassRealId`, `coe_le_coe_iff`, `Submodule.starProjection_le_starProjection_iff`, `instOrderIsoClassContinuousLinearMapIdOfNonUnitalAlgEquivClassOfStarHomClassOfContinuousMapClass`, `instStarOrderedRingRCLike`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antilipschitz_of_forall_le_inner_map` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Real` `Real.instLE` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `NNReal.toReal` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `funLike`	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NNReal.instInv`	—	`antilipschitz_of_bound` `NNReal.coe_inv` `inv_mul_eq_div` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_zero` `norm_zero` `MulZeroClass.zero_mul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `norm_pos_iff` `OrderIsoClass.map_le_map_iff` `OrderIso.instOrderIsoClass` `LE.le.trans` `mul_assoc` `sq` `norm_inner_le_norm` `Eq.le` `mul_comm`
`coe_le_coe_iff` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `LinearMap.instLoewnerPartialOrder` `toLinearMap` `ContinuousLinearMap` `instLoewnerPartialOrder`	—	`isPositive_toLinearMap_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`isPositive_adjoint_comp_self` 📖	mathematical	—	`IsPositive` `comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHomCompTriple.ids` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `ContinuousLinearMap` `toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `adjoint`	—	`IsPositive.adjoint_conj` `isPositive_one`
`isPositive_def` 📖	mathematical	—	`IsPositive` `LinearMap.IsSymmetric` `NormedAddCommGroup.toSeminormedAddCommGroup` `toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Real` `Real.instLE` `Real.instZero` `reApplyInnerSelf`	—	—
`isPositive_def'` 📖	mathematical	—	`IsPositive` `IsSelfAdjoint` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instStarId` `Real` `Real.instLE` `Real.instZero` `reApplyInnerSelf`	—	—
`isPositive_id` 📖	mathematical	—	`IsPositive` `id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	—	`LinearMap.isPositive_id`
`isPositive_iff` 📖	mathematical	—	`IsPositive` `LinearMap.IsSymmetric` `NormedAddCommGroup.toSeminormedAddCommGroup` `toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `ContinuousLinearMap` `funLike`	—	`LinearMap.isPositive_iff`
`isPositive_iff'` 📖	mathematical	—	`IsPositive` `IsSelfAdjoint` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instStarId` `Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `funLike`	—	—
`isPositive_iff_complex` 📖	mathematical	—	`IsPositive` `Complex` `Complex.instRCLike` `Complex.ofReal` `DFunLike.coe` `AddMonoidHom` `Real` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `funLike` `Real.instLE` `Real.instZero`	—	—
`isPositive_iff_eq_sum_rankOne` 📖	mathematical	—	`IsPositive` `Finset.sum` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.univ` `Fin.fintype` `DFunLike.coe` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `topologicalSpace` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `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` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `funLike` `addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `topologicalAddGroup` `toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `smulCommClass` `continuousConstSMul` `InnerProductSpace.rankOne`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `topologicalAddGroup` `RingHomIsometric.ids` `smulCommClass` `continuousConstSMul` `IsPositive.isSymmetric` `ext` `sum_apply` `Finset.sum_congr` `inner_smul_left` `smul_smul` `mul_assoc` `RCLike.conj_ofReal` `mul_comm` `LinearMap.IsPositive.isSymmetric` `IsPositive.toLinearMap` `Real.sqrt_mul` `LinearMap.IsPositive.nonneg_eigenvalues` `Real.sqrt_mul_self` `smul_assoc` `IsScalarTower.left` `LinearMap.IsSymmetric.apply_eigenvectorBasis` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `OrthonormalBasis.sum_repr` `isPositive_sum` `InnerProductSpace.isPositive_rankOne_self`
`isPositive_natCast` 📖	mathematical	—	`IsPositive` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instNatCast` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `isPositive_toLinearMap_iff` `LinearMap.isPositive_natCast`
`isPositive_ofNat` 📖	mathematical	—	`IsPositive`	—	`isPositive_natCast`
`isPositive_one` 📖	mathematical	—	`IsPositive` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `one`	—	`LinearMap.isPositive_one`
`isPositive_self_comp_adjoint` 📖	mathematical	—	`IsPositive` `comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHomCompTriple.ids` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `ContinuousLinearMap` `toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `adjoint`	—	`IsPositive.conj_adjoint` `isPositive_one`
`isPositive_sum` 📖	mathematical	`IsPositive`	`Finset.sum` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `isPositive_toLinearMap_iff` `coe_sum` `LinearMap.isPositive_sum`
`isPositive_toLinearMap_iff` 📖	mathematical	—	`LinearMap.IsPositive` `toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `IsPositive`	—	—
`isPositive_zero` 📖	mathematical	—	`IsPositive` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `zero`	—	`LinearMap.isPositive_zero`
`isUnit_of_forall_le_norm_inner_map` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Real` `Real.instLE` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `NNReal.toReal` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `funLike`	`IsUnit` `MonoidWithZero.toMonoid` `monoidWithZero`	—	`isUnit_iff_bijective` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomSurjective.invPair` `RingHomInvPair.ids` `bijective_iff_dense_range_and_antilipschitz` `RingHomIsometric.ids` `antilipschitz_of_forall_le_inner_map` `Submodule.topologicalClosure_eq_top_iff` `Submodule.eq_bot_iff` `le_antisymm` `norm_zero` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul` `le_of_lt` `Mathlib.Meta.Positivity.nnreal_coe_pos` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `isReduced_of_noZeroDivisors` `Nat.instCharZero`
`le_def` 📖	mathematical	—	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instLoewnerPartialOrder` `IsPositive` `sub` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	—
`nonneg_iff_isPositive` 📖	mathematical	—	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instLoewnerPartialOrder` `zero` `IsPositive`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `sub_zero` `le_def`

ContinuousLinearMap.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPositive_iff_isSelfAdjoint` 📖	mathematical	`IsIdempotentElem` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.instMul`	`ContinuousLinearMap.IsPositive` `IsSelfAdjoint` `ContinuousLinearMap.instStarId`	—	`ContinuousLinearMap.isPositive_toLinearMap_iff` `LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric` `toLinearMap` `ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric`

ContinuousLinearMap.IsPositive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.isPositive_toLinearMap_iff` `LinearMap.IsPositive.add` `toLinearMap`
`adjoint_conj` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHomCompTriple.ids` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `ContinuousLinearMap` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `ContinuousLinearMap.adjoint`	—	`RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.adjoint_adjoint` `conj_adjoint`
`conj_adjoint` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHomCompTriple.ids` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `ContinuousLinearMap` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `ContinuousLinearMap.adjoint`	—	`RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.isPositive_def'` `IsSelfAdjoint.conj_adjoint` `isSelfAdjoint` `ContinuousLinearMap.reApplyInnerSelf.eq_1` `ContinuousLinearMap.comp_apply` `ContinuousLinearMap.adjoint_inner_right` `re_inner_nonneg_left`
`conj_starProjection` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHomCompTriple.ids` `Submodule.starProjection`	—	`RingHomCompTriple.ids` `Submodule.starProjection_isSymmetric` `isSymmetric` `inner_nonneg_right`
`inner_left_eq_inner_right` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.funLike`	—	`isSymmetric`
`inner_nonneg_left` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.funLike`	—	`LinearMap.IsPositive.inner_nonneg_left` `toLinearMap`
`inner_nonneg_right` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.funLike`	—	`LinearMap.IsPositive.inner_nonneg_right` `toLinearMap`
`isSelfAdjoint` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`IsSelfAdjoint` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.instStarId`	—	`LinearMap.IsSymmetric.isSelfAdjoint` `isSymmetric`
`isSymmetric` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`LinearMap.IsSymmetric` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	—	—
`of_isStarProjection` 📖	mathematical	`IsStarProjection` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.instMul` `ContinuousLinearMap.instStarId`	`ContinuousLinearMap.IsPositive`	—	`ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint` `IsStarProjection.isIdempotentElem` `IsStarProjection.isSelfAdjoint`
`orthogonalProjection_comp` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `Submodule.normedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceSubtype` `Submodule.addCommMonoid` `Submodule.module` `RingHomCompTriple.ids` `Submodule.orthogonalProjection` `Submodule.subtypeL`	—	`RingHomCompTriple.ids` `Submodule.inner_orthogonalProjection_eq_of_mem_right` `Submodule.inner_orthogonalProjection_eq_of_mem_left` `isSymmetric` `inner_nonneg_right`
`re_inner_nonneg_left` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.funLike`	—	—
`re_inner_nonneg_right` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.funLike`	—	`LinearMap.IsPositive.re_inner_nonneg_right` `toLinearMap`
`smul_of_nonneg` 📖	mathematical	`ContinuousLinearMap.IsPositive` `Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul`	—	`smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.isPositive_toLinearMap_iff` `LinearMap.IsPositive.smul_of_nonneg` `toLinearMap`
`toLinearMap` 📖	mathematical	`ContinuousLinearMap.IsPositive`	`LinearMap.IsPositive` `ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	—	`ContinuousLinearMap.isPositive_toLinearMap_iff`

InnerProductSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPositive_rankOne_self` 📖	mathematical	—	`ContinuousLinearMap.IsPositive` `DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `RCLike.toStarRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedSpace.toModule` `toNormedSpace` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `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` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `rankOne`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `inner_smul_left` `RCLike.conj_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPositive_symm_iff` 📖	mathematical	—	`LinearMap.IsPositive` `toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `symm`	—	`RingHomInvPair.ids` `LinearMap.IsPositive.toLinearMap_symm`

LinearMap

Definitions

Name	Category	Theorems
`IsPositive` 📖	MathDef	23 math math: `isPositive_adjoint_comp_self`, `ContinuousLinearMap.IsPositive.toLinearMap`, `isPositive_id`, `IsSymmetricProjection.isPositive`, `nonneg_iff_isPositive`, `IsPositive.of_isSymmetricProjection`, `ContinuousLinearMap.isPositive_toLinearMap_iff`, `isPositive_ofNat`, `isPositive_natCast`, `LinearEquiv.isPositive_symm_iff`, `isPositive_linearIsometryEquiv_conj_iff`, `isPositive_toContinuousLinearMap_iff`, `Matrix.isPositive_toEuclideanLin_iff`, `le_def`, `isPositive_self_comp_adjoint`, `isPositive_iff_complex`, `isPositive_zero`, `IsPositive.of_isStarProjection`, `isPositive_iff`, `ProbabilityTheory.isPositive_covarianceOperator`, `posSemidef_toMatrix_iff`, `isPositive_one`, `IsIdempotentElem.isPositive_iff_isSymmetric`
`instLoewnerPartialOrder` 📖	CompOp	4 math math: `nonneg_iff_isPositive`, `le_def`, `ContinuousLinearMap.coe_le_coe_iff`, `IsSymmetricProjection.le_iff_range_le_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPositive_adjoint_comp_self` 📖	mathematical	—	`IsPositive` `comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `adjoint`	—	`IsPositive.adjoint_conj` `isPositive_one`
`isPositive_id` 📖	mathematical	—	`IsPositive` `id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	—	`isPositive_one`
`isPositive_iff` 📖	mathematical	—	`IsPositive` `IsSymmetric` `NormedAddCommGroup.toSeminormedAddCommGroup` `Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instFunLike`	—	`RCLike.ofReal_nonneg` `IsSymmetric.coe_re_inner_apply_self`
`isPositive_iff_complex` 📖	mathematical	—	`IsPositive` `Complex` `Complex.instRCLike` `Complex.ofReal` `DFunLike.coe` `AddMonoidHom` `Real` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `LinearMap` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `instFunLike` `Real.instLE` `Real.instZero`	—	—
`isPositive_linearIsometryEquiv_conj_iff` 📖	mathematical	—	`IsPositive` `comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearIsometryEquiv.toLinearEquiv` `LinearIsometryEquiv.symm`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearIsometryEquiv.inner_map_eq_flip` `LinearIsometryEquiv.symm_apply_apply`
`isPositive_natCast` 📖	mathematical	—	`IsPositive` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Module.End.instRing` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsSymmetric.natCast` `Nat.cast_smul_eq_nsmul` `inner_smul_left` `map_natCast` `RingHom.instRingHomClass` `RCLike.mul_re` `RCLike.natCast_re` `inner_self_im` `MulZeroClass.mul_zero` `sub_zero` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `inner_self_nonneg`
`isPositive_ofNat` 📖	mathematical	—	`IsPositive`	—	`isPositive_natCast`
`isPositive_one` 📖	mathematical	—	`IsPositive` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.End.instOne`	—	`IsSymmetric.id` `inner_self_nonneg`
`isPositive_self_comp_adjoint` 📖	mathematical	—	`IsPositive` `comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `adjoint`	—	`IsPositive.conj_adjoint` `isPositive_one`
`isPositive_sum` 📖	mathematical	`IsPositive`	`Finset.sum` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `addCommMonoid`	—	`isSymmetric_sum` `IsPositive.isSymmetric` `coe_sum` `Finset.sum_apply` `sum_inner` `map_sum` `AddMonoidHom.instAddMonoidHomClass` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsPositive.re_inner_nonneg_left`
`isPositive_toContinuousLinearMap_iff` 📖	mathematical	—	`ContinuousLinearMap.IsPositive` `DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `addCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `ContinuousSMul.continuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.continuousSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toContinuousLinearMap` `RCLike.toCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `IsPositive`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `RCLike.toCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`isPositive_zero` 📖	mathematical	—	`IsPositive` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instZero`	—	`IsSymmetric.zero` `inner_zero_left` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`
`le_def` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instLoewnerPartialOrder` `IsPositive` `instSub` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`nonneg_iff_isPositive` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instLoewnerPartialOrder` `instZero` `IsPositive`	—	`sub_zero` `le_def`
`posSemidef_toMatrix_iff` 📖	mathematical	—	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Matrix` `addCommMonoid` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toMatrix` `Finite.of_fintype` `OrthonormalBasis.toBasis` `IsPositive`	—	`RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `fact_one_le_two_ennreal` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `Matrix.isPositive_toEuclideanLin_iff` `RingHomCompTriple.ids` `ext` `PiLp.ext` `Nat.instAtLeastTwoHAddOfNat` `LinearEquiv.trans.congr_simp` `LinearEquiv.arrowCongr.congr_simp` `OrthonormalBasis.coe_toBasis_repr` `Matrix.toLin'_toMatrix'` `isPositive_linearIsometryEquiv_conj_iff`

LinearMap.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPositive_iff_isSymmetric` 📖	mathematical	`IsIdempotentElem` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.End.instMul`	`LinearMap.IsPositive` `LinearMap.IsSymmetric`	—	`LinearMap.IsPositive.isSymmetric` `IsIdempotentElem.eq` `Module.End.mul_apply` `inner_self_nonneg`

LinearMap.IsPositive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`LinearMap.IsPositive`	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instAdd`	—	`LinearMap.IsSymmetric.add` `isSymmetric` `LinearMap.add_apply` `inner_add_left` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `re_inner_nonneg_left`
`adjoint_conj` 📖	mathematical	`LinearMap.IsPositive`	`LinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.adjoint`	—	`RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `LinearMap.adjoint_adjoint` `conj_adjoint`
`adjoint_eq` 📖	mathematical	`LinearMap.IsPositive`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.adjoint`	—	`isSelfAdjoint`
`conj_adjoint` 📖	mathematical	`LinearMap.IsPositive`	`LinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.adjoint`	—	`FiniteDimensional.complete` `RCLike.toCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousSMul.continuousConstSMul` `ContinuousLinearMap.IsPositive.conj_adjoint` `LinearMap.isPositive_toContinuousLinearMap_iff`
`inner_nonneg_left` 📖	mathematical	`LinearMap.IsPositive`	`Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instFunLike`	—	`LinearMap.isPositive_iff`
`inner_nonneg_right` 📖	mathematical	`LinearMap.IsPositive`	`Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instFunLike`	—	`inner_nonneg_left` `isSymmetric`
`isPositive_smul_iff` 📖	mathematical	`LinearMap.IsPositive`	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`smulCommClass_self` `ne_zero_iff` `inner_smul_right` `inner_nonneg_right` `le_of_smul_le_smul_of_pos_right` `MulPosReflectLE.toSMulPosReflectLE` `RCLike.instMulPosReflectLE` `MulZeroClass.zero_mul` `smul_of_nonneg`
`isSelfAdjoint` 📖	mathematical	`LinearMap.IsPositive`	`IsSelfAdjoint` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instStarId`	—	`LinearMap.isSymmetric_iff_isSelfAdjoint` `isSymmetric`
`isSymmetric` 📖	mathematical	`LinearMap.IsPositive`	`LinearMap.IsSymmetric` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—
`ne_zero_iff` 📖	mathematical	`LinearMap.IsPositive`	`Preorder.toLT` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instFunLike`	—	`LinearMap.IsSymmetric.inner_map_self_eq_zero` `isSymmetric` `inner_nonneg_left`
`nonneg_eigenvalues` 📖	mathematical	`LinearMap.IsPositive` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	`Real` `Real.instLE` `Real.instZero` `LinearMap.IsSymmetric.eigenvalues` `isSymmetric`	—	`isSymmetric` `LinearMap.IsSymmetric.apply_eigenvectorBasis` `inner_smul_real_left` `RCLike.smul_re` `inner_self_eq_norm_sq` `OrthonormalBasis.norm_eq_one` `one_pow` `mul_one`
`of_isStarProjection` 📖	mathematical	`LinearMap.IsSymmetricProjection` `NormedAddCommGroup.toSeminormedAddCommGroup`	`LinearMap.IsPositive`	—	`LinearMap.IsSymmetricProjection.isPositive`
`of_isSymmetricProjection` 📖	mathematical	`LinearMap.IsSymmetricProjection` `NormedAddCommGroup.toSeminormedAddCommGroup`	`LinearMap.IsPositive`	—	`LinearMap.IsSymmetricProjection.isPositive`
`re_inner_nonneg_left` 📖	mathematical	`LinearMap.IsPositive`	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instFunLike`	—	—
`re_inner_nonneg_right` 📖	mathematical	`LinearMap.IsPositive`	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instFunLike`	—	`re_inner_nonneg_left` `inner_re_symm`
`smul_of_nonneg` 📖	mathematical	`LinearMap.IsPositive` `Preorder.toLE` `PartialOrder.toPreorder` `RCLike.toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing`	—	`RCLike.le_iff_re_im` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `smulCommClass_self` `LinearMap.IsSymmetric.smul` `LinearMap.smul_apply` `inner_smul_left` `RCLike.mul_re` `RCLike.conj_eq_iff_im` `MulZeroClass.zero_mul` `sub_zero` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `RCLike.re_nonneg_of_nonneg` `re_inner_nonneg_left`
`toLinearMap_symm` 📖	mathematical	`LinearMap.IsPositive` `LinearEquiv.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	`LinearEquiv.symm`	—	`RingHomInvPair.ids` `LinearMap.IsSymmetric.toLinearMap_symm` `isSymmetric` `LinearEquiv.apply_symm_apply` `LinearEquiv.coe_toLinearMap`

LinearMap.IsSymmetricProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPositive` 📖	mathematical	`LinearMap.IsSymmetricProjection` `NormedAddCommGroup.toSeminormedAddCommGroup`	`LinearMap.IsPositive`	—	`LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric` `isIdempotentElem` `isSymmetric`
`le_iff_range_le_range` 📖	mathematical	`LinearMap.IsSymmetricProjection` `NormedAddCommGroup.toSeminormedAddCommGroup`	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `LinearMap.instLoewnerPartialOrder` `Submodule` `Submodule.instPartialOrder` `LinearMap.range` `RingHomSurjective.ids`	—	`RingHomSurjective.ids` `isIdempotentElem` `Module.End.mul_apply` `isSymmetric` `inner_self_eq_norm_sq` `LinearMap.isSymmetricProjection_iff_eq_coe_starProjection` `Submodule.isCompl_orthogonal_of_hasOrthogonalProjection` `LinearMap.range.congr_simp` `Submodule.toLinearMap_starProjection_eq_isComplProjection` `Submodule.IsCompl.projection_range` `Submodule.mem_iff_norm_starProjection` `le_antisymm` `Submodule.norm_starProjection_apply_le` `abs_norm` `Real.instIsStrictOrderedRing` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LinearMap.IsIdempotentElem.mem_range_iff` `map_sub` `AddMonoidHom.instAddMonoidHomClass` `inner_sub_left` `isPositive` `sub_of_range_le_range`

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPositive_toEuclideanLin_iff` 📖	mathematical	—	`LinearMap.IsPositive` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `WithLp.instModule` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toEuclideanLin` `PosSemidef` `RCLike.toPartialOrder` `RCLike.toStarRing`	—	`fact_one_le_two_ennreal` `RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `Nat.instAtLeastTwoHAddOfNat` `inner_re_symm` `dotProduct_comm` `RCLike.nonneg_iff` `Equiv.forall_congr'` `IsHermitian.im_star_dotProduct_mulVec_self`
`posSemidef_iff_eq_sum_vecMulVec` 📖	mathematical	—	`PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `Finset.sum` `Matrix` `addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Finset.univ` `Fin.fintype` `vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`fact_one_le_two_ennreal` `RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `isPositive_toEuclideanLin_iff` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `RCLike.toCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `LinearMap.isPositive_toContinuousLinearMap_iff` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `ContinuousLinearMap.isPositive_iff_eq_sum_rankOne` `ContinuousLinearMap.coe_sum` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Finset.sum_congr` `InnerProductSpace.symm_toEuclideanLin_rankOne` `Nat.instAtLeastTwoHAddOfNat`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`starProjection_inj` 📖	mathematical	—	`starProjection`	—	—
`starProjection_le_starProjection_iff` 📖	mathematical	—	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `ContinuousLinearMap.instLoewnerPartialOrder` `starProjection` `Submodule` `instPartialOrder`	—	`RingHomSurjective.ids` `LinearMap.IsSymmetricProjection.le_iff_range_le_range` `isSymmetricProjection_starProjection` `isCompl_orthogonal_of_hasOrthogonalProjection` `LinearMap.range.congr_simp` `toLinearMap_starProjection_eq_isComplProjection` `IsCompl.projection_range`

---

← Back to Index