Documentation Verification Report

Order

📁 Source: Mathlib/Analysis/Matrix/Order.lean

Statistics

Metric	Count
Definitions `matrixInnerProductSpace`, `matrixNormedAddCommGroup`, `instPartialOrder`, `instPreOrder`, `toMatrixInnerProductSpace`, `toMatrixNormedAddCommGroup`, `toMatrixSeminormedAddCommGroup`, `tracePositiveLinearMap`	8
Theorems `det_abs`, `posDef`, `posSemidef`, `commute_iff`, `isStrictlyPositive`, `kronecker`, `posDef_sqrt`, `det_sqrt`, `dotProduct_mulVec_zero_iff`, `inv_sqrt`, `kronecker`, `nonneg`, `posDef_iff_isUnit`, `toLinearMap₂'_zero_iff`, `instIsOrderedAddMonoid`, `instNonnegSpectrumClass`, `instStarOrderedRing`, `isStrictlyPositive_iff_posDef`, `le_iff`, `nonneg_iff_posSemidef`, `posDef_iff_eq_conjTranspose_mul_self`, `posSemidef_iff_isHermitian_and_spectrum_nonneg`, `toLinearMap_tracePositiveLinearMap`, `tracePositiveLinearMap_apply`	24
Total	32

Matrix

Definitions

Name	Category	Theorems
`instPartialOrder` 📖	CompOp	8 math math: `IsHermitian.det_abs`, `toLinearMap_tracePositiveLinearMap`, `PosSemidef.det_sqrt`, `instNonnegSpectrumClass`, `PosSemidef.inv_sqrt`, `instStarOrderedRing`, `PosDef.posDef_sqrt`, `tracePositiveLinearMap_apply`
`instPreOrder` 📖	CompOp	6 math math: `le_iff`, `PosSemidef.nonneg`, `nonneg_iff_posSemidef`, `isStrictlyPositive_iff_posDef`, `PosDef.isStrictlyPositive`, `instIsOrderedAddMonoid`
`toMatrixInnerProductSpace` 📖	CompOp	—
`toMatrixNormedAddCommGroup` 📖	CompOp	—
`toMatrixSeminormedAddCommGroup` 📖	CompOp	—
`tracePositiveLinearMap` 📖	CompOp	2 math math: `toLinearMap_tracePositiveLinearMap`, `tracePositiveLinearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `Matrix` `addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instPreOrder`	—	`le_iff` `add_sub_add_right_eq_sub`
`instNonnegSpectrumClass` 📖	mathematical	—	`NonnegSpectrumClass` `Real` `Matrix` `Real.instCommSemiring` `Real.partialOrder` `instNonUnitalRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `instPartialOrder` `module` `CommSemiring.toSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`quasispectrum_eq_spectrum_union_zero` `Set.union_singleton` `LE.le.posSemidef` `Set.ext_iff` `IsHermitian.spectrum_real_eq_range_eigenvalues` `PosSemidef.eigenvalues_nonneg`
`instStarOrderedRing` 📖	mathematical	—	`StarOrderedRing` `Matrix` `nonUnitalSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `instPartialOrder` `instStarRing` `RCLike.toStarRing`	—	`StarOrderedRing.of_nonneg_iff'` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts` `IsScalarTower.right` `Algebra.to_smulCommClass` `ContinuousFunctionalCalculus.toNonUnital` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `IsHermitian.instContinuousFunctionalCalculus` `PosSemidef.isHermitian` `QuasispectrumRestricts.nnreal_of_nonneg` `instNonnegSpectrumClass` `PosSemidef.nonneg` `sub_zero` `IsSelfAdjoint.star_eq` `posSemidef_conjTranspose_mul_self` `Finite.of_fintype` `RCLike.toStarOrderedRing`
`isStrictlyPositive_iff_posDef` 📖	mathematical	—	`IsStrictlyPositive` `Matrix` `Preorder.toLE` `instPreOrder` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `RCLike.toPartialOrder` `RCLike.toStarRing`	—	`PosSemidef.posDef_iff_isUnit` `LE.le.posSemidef` `IsStrictlyPositive.nonneg` `IsStrictlyPositive.isUnit` `IsUnit.isStrictlyPositive` `PosDef.isUnit` `PosSemidef.nonneg` `PosDef.posSemidef`
`le_iff` 📖	mathematical	—	`Matrix` `Preorder.toLE` `instPreOrder` `PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	—
`nonneg_iff_posSemidef` 📖	mathematical	—	`Matrix` `Preorder.toLE` `instPreOrder` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `RCLike.toPartialOrder` `RCLike.toStarRing`	—	`le_iff` `sub_zero`
`posDef_iff_eq_conjTranspose_mul_self` 📖	mathematical	—	`PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `Matrix` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`isStrictlyPositive_iff_posDef` `CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self` `instStarOrderedRing` `IsHermitian.instContinuousFunctionalCalculus` `instNonnegSpectrumClass` `IsTopologicalRing.toIsSemitopologicalRing` `topologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`posSemidef_iff_isHermitian_and_spectrum_nonneg` 📖	mathematical	—	`PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `StarRing.toStarAddMonoid` `Set` `Set.instHasSubset` `spectrum` `Matrix` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `instRing` `instAlgebra` `Ring.toSemiring` `Algebra.id` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`PosSemidef.isHermitian` `IsHermitian.spectrum_eq_image_range` `Nat.cast_zero` `algebraMap.coe_zero` `PosSemidef.eigenvalues_nonneg` `IsHermitian.posSemidef_iff_eigenvalues_nonneg` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`toLinearMap_tracePositiveLinearMap` 📖	mathematical	—	`PositiveLinearMap.toLinearMap` `Matrix` `addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instPartialOrder` `RCLike.toPartialOrder` `module` `tracePositiveLinearMap` `traceLinearMap`	—	—
`tracePositiveLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `PositiveLinearMap` `Matrix` `addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instPartialOrder` `RCLike.toPartialOrder` `module` `PositiveLinearMap.instFunLike` `tracePositiveLinearMap` `trace`	—	—

Matrix.IsHermitian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_abs` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `StarRing.toStarAddMonoid` `RCLike.toStarRing`	`Matrix.det` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `CFC.abs` `Matrix` `Matrix.instNonUnitalRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Matrix.instStarRing` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `RCLike.toStarRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Matrix.module` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Algebra.to_smulCommClass` `Real.instCommSemiring` `Matrix.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Matrix.instAlgebra` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `IsScalarTower.right` `ContinuousFunctionalCalculus.toNonUnital` `IsSelfAdjoint` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `StarRing.toStarAddMonoid` `Real.instField` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.instRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Semifield.toCommSemiring` `Ring.toSemiring` `instContinuousFunctionalCalculus` `Matrix.instPartialOrder` `Matrix.instStarOrderedRing` `Matrix.instNonnegSpectrumClass` `RCLike.ofReal` `Norm.norm` `NormedField.toNorm`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `ContinuousFunctionalCalculus.toNonUnital` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `instContinuousFunctionalCalculus` `Matrix.instStarOrderedRing` `Matrix.instNonnegSpectrumClass` `CFC.abs_eq_cfc_norm` `Matrix.topologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `cfc_eq` `Matrix.det_map` `instAlgEquivClassOfNonUnitalAlgEquivClass` `StarAlgEquiv.instNonUnitalAlgEquivClass` `Matrix.det_diagonal` `Finset.prod_congr` `det_eq_prod_eigenvalues` `norm_prod` `NormedDivisionRing.toNormMulClass` `NormedDivisionRing.to_normOneClass` `norm_algebraMap'` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

Matrix.IsStrictlyPositive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`posDef` 📖	mathematical	`IsStrictlyPositive` `Matrix` `Preorder.toLE` `Matrix.instPreOrder` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	—	`Matrix.isStrictlyPositive_iff_posDef`

Matrix.LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`posSemidef` 📖	mathematical	`Matrix` `Preorder.toLE` `Matrix.instPreOrder` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	—	`Matrix.nonneg_iff_posSemidef`

Matrix.PosDef

Definitions

Name	Category	Theorems
`matrixInnerProductSpace` 📖	CompOp	—
`matrixNormedAddCommGroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_iff` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Commute` `Matrix` `Matrix.instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `RCLike.toPartialOrder` `RCLike.toStarRing` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid`	—	`IsStrictlyPositive.commute_iff` `Matrix.instStarOrderedRing` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass` `isStrictlyPositive` `Matrix.isStrictlyPositive_iff_posDef`
`isStrictlyPositive` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`IsStrictlyPositive` `Matrix` `Preorder.toLE` `Matrix.instPreOrder` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`Matrix.isStrictlyPositive_iff_posDef`
`kronecker` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `Matrix.kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`Matrix.PosSemidef.posDef_iff_isUnit` `Matrix.PosSemidef.kronecker` `posSemidef` `Matrix.IsUnit.kronecker` `isUnit`
`posDef_sqrt` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `CFC.sqrt` `Matrix` `Matrix.instPartialOrder` `Matrix.instNonUnitalRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Matrix.instStarRing` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Matrix.module` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Algebra.to_smulCommClass` `Real.instCommSemiring` `Matrix.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Matrix.instAlgebra` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `IsScalarTower.right` `Matrix.instStarOrderedRing` `ContinuousFunctionalCalculus.toNonUnital` `IsSelfAdjoint` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `StarRing.toStarAddMonoid` `Real.instField` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.instRing` `Semifield.toCommSemiring` `Ring.toSemiring` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass`	—	`Matrix.IsStrictlyPositive.posDef` `Algebra.to_smulCommClass` `IsScalarTower.right` `Matrix.instStarOrderedRing` `ContinuousFunctionalCalculus.toNonUnital` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass` `IsStrictlyPositive.sqrt` `IsTopologicalRing.toIsSemitopologicalRing` `Matrix.topologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `isStrictlyPositive`

Matrix.PosSemidef

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_sqrt` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Matrix.det` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `CFC.sqrt` `Matrix` `Matrix.instPartialOrder` `Matrix.instNonUnitalRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Matrix.instStarRing` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `RCLike.toStarRing` `Matrix.module` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Algebra.to_smulCommClass` `Real.instCommSemiring` `Matrix.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Matrix.instAlgebra` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `IsScalarTower.right` `Matrix.instStarOrderedRing` `ContinuousFunctionalCalculus.toNonUnital` `IsSelfAdjoint` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `StarRing.toStarAddMonoid` `Real.instField` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.instRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Semifield.toCommSemiring` `Ring.toSemiring` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass` `RCLike.sqrt`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `Matrix.instStarOrderedRing` `ContinuousFunctionalCalculus.toNonUnital` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass` `NNReal.instIsTopologicalSemiring` `NNReal.instContinuousStar` `Nonneg.instContinuousFunctionalCalculus` `CFC.sqrt_eq_cfc` `IsTopologicalRing.toIsSemitopologicalRing` `Matrix.topologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `cfc_nnreal_eq_real` `nonneg` `Matrix.IsHermitian.cfc_eq` `RCLike.sqrt_of_nonneg` `det_nonneg` `Matrix.det.congr_simp` `Real.coe_sqrt` `Matrix.det_map` `instAlgEquivClassOfNonUnitalAlgEquivClass` `StarAlgEquiv.instNonUnitalAlgEquivClass` `Matrix.det_diagonal` `Finset.prod_congr` `isHermitian` `Matrix.IsHermitian.det_eq_prod_eigenvalues` `RCLike.ofReal_re` `Real.sqrt_prod` `eigenvalues_nonneg`
`dotProduct_mulVec_zero_iff` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `RCLike.toStarRing` `Matrix.mulVec` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Pi.instZero`	—	`CStarAlgebra.nonneg_iff_eq_star_mul_self` `Algebra.to_smulCommClass` `IsScalarTower.right` `Matrix.instStarOrderedRing` `ContinuousFunctionalCalculus.toNonUnital` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass` `IsTopologicalRing.toIsSemitopologicalRing` `Matrix.topologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `nonneg` `RCLike.toStarOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `star_star` `Matrix.vecMul_conjTranspose` `Matrix.dotProduct_mulVec` `Matrix.mulVec_zero` `dotProduct_zero`
`inv_sqrt` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Matrix` `Matrix.inv` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `CFC.sqrt` `Matrix.instPartialOrder` `Matrix.instNonUnitalRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Matrix.instStarRing` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `RCLike.toStarRing` `Matrix.module` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Algebra.to_smulCommClass` `Real.instCommSemiring` `Matrix.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Matrix.instAlgebra` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `IsScalarTower.right` `Matrix.instStarOrderedRing` `ContinuousFunctionalCalculus.toNonUnital` `IsSelfAdjoint` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `StarRing.toStarAddMonoid` `Real.instField` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.instRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Semifield.toCommSemiring` `Ring.toSemiring` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `Matrix.instStarOrderedRing` `ContinuousFunctionalCalculus.toNonUnital` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass` `CFC.sqrt_eq_iff` `IsTopologicalRing.toIsSemitopologicalRing` `Matrix.topologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `nonneg` `inv` `Matrix.LE.le.posSemidef` `CFC.sqrt_nonneg` `sq` `Matrix.inv_pow'` `CFC.sq_sqrt`
`kronecker` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `Matrix.kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`CStarAlgebra.nonneg_iff_eq_star_mul_self` `Algebra.to_smulCommClass` `IsScalarTower.right` `Matrix.instStarOrderedRing` `ContinuousFunctionalCalculus.toNonUnital` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass` `IsTopologicalRing.toIsSemitopologicalRing` `Matrix.topologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `nonneg` `Matrix.mul_kronecker_mul` `Matrix.posSemidef_conjTranspose_mul_self` `Finite.instProd` `RCLike.toStarOrderedRing`
`nonneg` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Matrix` `Preorder.toLE` `Matrix.instPreOrder` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`Matrix.nonneg_iff_posSemidef`
`posDef_iff_isUnit` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing` `IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`Matrix.PosDef.isUnit` `Matrix.PosDef.of_dotProduct_mulVec_pos` `CStarAlgebra.nonneg_iff_eq_star_mul_self` `Algebra.to_smulCommClass` `IsScalarTower.right` `Matrix.instStarOrderedRing` `ContinuousFunctionalCalculus.toNonUnital` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `Matrix.IsHermitian.instContinuousFunctionalCalculus` `Matrix.instNonnegSpectrumClass` `IsTopologicalRing.toIsSemitopologicalRing` `Matrix.topologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `nonneg` `Matrix.dotProduct_mulVec` `RCLike.toStarOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Mathlib.Tactic.Contrapose.contrapose₄` `map_eq_zero_iff` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Matrix.mulVec_injective_iff_isUnit` `Matrix.mulVecLin_apply` `Matrix.mulVec_mulVec` `Matrix.mulVec_zero`
`toLinearMap₂'_zero_iff` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Pi.Function.module` `Semiring.toModule` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `Matrix.addCommMonoid` `Matrix.module` `LinearMap.instSMulCommClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Matrix.toLinearMap₂'` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `RCLike.toStarRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Matrix.mulVec` `Pi.instZero`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids` `LinearMap.instSMulCommClass` `Matrix.toLinearMap₂'_apply'` `dotProduct_mulVec_zero_iff`

---

← Back to Index