Documentation Verification Report

CompletelyPositiveMap

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

Statistics

Metric	Count
Definitions `«term_→CP_»`, `CompletelyPositiveMap`, `instFunLike`, `toLinearMap`, `CompletelyPositiveMapClass`, `instCoeToCompletelyPositiveMap`, `toCompletelyPositiveLinearMap`	7
Theorems `instCompletelyPositiveMapClass`, `instLinearMapClassComplex`, `map_cstarMatrix_nonneg`, `map_cstarMatrix_nonneg'`, `instOrderHomClass`, `map_cstarMatrix_nonneg'`, `instCompletelyPositiveMapClass`, `of_map_cstarMatrix_nonneg`	8
Total	15

CStarAlgebra

Definitions

Name	Category	Theorems
`«term_→CP_»` 📖	CompOp	—

CompletelyPositiveMap

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	3 math math: `map_cstarMatrix_nonneg`, `instLinearMapClassComplex`, `instCompletelyPositiveMapClass`
`toLinearMap` 📖	CompOp	1 math math: `map_cstarMatrix_nonneg'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompletelyPositiveMapClass` 📖	mathematical	—	`CompletelyPositiveMapClass` `CompletelyPositiveMap` `instFunLike`	—	`map_cstarMatrix_nonneg'`
`instLinearMapClassComplex` 📖	mathematical	—	`LinearMapClass` `CompletelyPositiveMap` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `instFunLike`	—	`map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `MulActionSemiHomClass.map_smulₛₗ` `SemilinearMapClass.toMulActionSemiHomClass`
`map_cstarMatrix_nonneg` 📖	mathematical	`CStarMatrix` `Preorder.toLE` `PartialOrder.toPreorder` `CStarMatrix.instPartialOrder` `CStarMatrix.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing`	`CStarMatrix.map` `DFunLike.coe` `CompletelyPositiveMap` `instFunLike`	—	`ContinuousSemilinearMapClass.toSemilinearMapClass` `PositiveLinearMap.instContinuousLinearMapClassComplexOfLinearMapClassOfOrderHomClass` `instLinearMapClassComplex` `CompletelyPositiveMapClass.instOrderHomClass` `instCompletelyPositiveMapClass` `CompletelyPositiveMapClass.map_cstarMatrix_nonneg'` `map_nonneg` `StarRingHomClass.instOrderHomClass` `CStarMatrix.instStarOrderedRing` `NonUnitalAlgHomClass.toNonUnitalRingHomClass` `instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass` `StarAlgEquiv.instNonUnitalAlgEquivClass` `NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass` `NonUnitalStarRingHomClass.toStarHomClass` `RingEquivClass.toNonUnitalRingHomClass` `NonUnitalAlgEquivClass.toRingEquivClass` `StarRingEquivClass.instNonUnitalStarRingHomClass` `StarAlgEquiv.instStarRingEquivClass` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `CStarMatrix.reindexₐ_symm` `StarAlgEquiv.symm_apply_apply` `CStarMatrix.mapₗ_reindexₐ`
`map_cstarMatrix_nonneg'` 📖	mathematical	`CStarMatrix` `Preorder.toLE` `PartialOrder.toPreorder` `CStarMatrix.instPartialOrder` `Fin.fintype` `CStarMatrix.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing`	`CStarMatrix.map` `DFunLike.coe` `LinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `LinearMap.instFunLike` `toLinearMap`	—	—

CompletelyPositiveMapClass

Definitions

Name	Category	Theorems
`instCoeToCompletelyPositiveMap` 📖	CompOp	—
`toCompletelyPositiveLinearMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instOrderHomClass` 📖	mathematical	—	`OrderHomClass` `Preorder.toLE` `PartialOrder.toPreorder`	—	`OrderHomClass.of_map_cstarMatrix_nonneg` `map_cstarMatrix_nonneg'`
`map_cstarMatrix_nonneg'` 📖	mathematical	`CStarMatrix` `Preorder.toLE` `PartialOrder.toPreorder` `CStarMatrix.instPartialOrder` `Fin.fintype` `CStarMatrix.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing`	`CStarMatrix.map` `DFunLike.coe`	—	—

NonUnitalStarAlgHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompletelyPositiveMapClass` 📖	mathematical	—	`CompletelyPositiveMapClass`	—	`map_nonneg` `StarRingHomClass.instOrderHomClass` `CStarMatrix.instStarOrderedRing` `NonUnitalAlgHomClass.toNonUnitalRingHomClass` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `instNonUnitalStarRingHomClassOfStarHomClass` `NonUnitalStarAlgHom.instStarHomClass` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass`

OrderHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_map_cstarMatrix_nonneg` 📖	mathematical	`CStarMatrix` `Preorder.toLE` `PartialOrder.toPreorder` `CStarMatrix.instPartialOrder` `Fin.fintype` `CStarMatrix.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarMatrix.map` `DFunLike.coe`	`OrderHomClass`	—	`of_addMonoidHom` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `map_nonneg` `StarRingHomClass.instOrderHomClass` `CStarMatrix.instStarOrderedRing` `NonUnitalAlgHomClass.toNonUnitalRingHomClass` `instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass` `StarAlgEquiv.instNonUnitalAlgEquivClass` `NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass` `PositiveLinearMap.instStarHomClassOfLinearMapClassComplexOfOrderHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `NonUnitalStarAlgHom.instContinuousLinearMapClassComplex` `NonUnitalStarRingHomClass.toStarHomClass` `RingEquivClass.toNonUnitalRingHomClass` `NonUnitalAlgEquivClass.toRingEquivClass` `StarRingEquivClass.instNonUnitalStarRingHomClass` `StarAlgEquiv.instStarRingEquivClass` `OrderIsoClass.toOrderHomClass` `StarRingEquivClass.instOrderIsoClass` `AddMonoidHomClass.toZeroHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass`

(root)

Definitions

Name	Category	Theorems
`CompletelyPositiveMap` 📖	CompData	3 math math: `CompletelyPositiveMap.map_cstarMatrix_nonneg`, `CompletelyPositiveMap.instLinearMapClassComplex`, `CompletelyPositiveMap.instCompletelyPositiveMapClass`
`CompletelyPositiveMapClass` 📖	CompData	2 math math: `NonUnitalStarAlgHomClass.instCompletelyPositiveMapClass`, `CompletelyPositiveMap.instCompletelyPositiveMapClass`

---

← Back to Index