Documentation Verification Report

PositiveLinearMap

📁 Source: Mathlib/Algebra/Order/Module/PositiveLinearMap.lean

Statistics

Metric	Count
Definitions `instAdd`, `instAddCommMonoid`, `instFunLike`, `instSMulNat`, `instZero`, `mk₀`, `toLinearMap`, `toOrderHom`, `instCoeToLinearMap`, `toPositiveLinearMap`, `«term_→ₚ[_]_»`	11
Theorems `ofLinear`, `of_addMonoidHom`, `add_apply`, `coe_toLinearMap`, `ext`, `ext_iff`, `instLinearMapClass`, `instOrderHomClass`, `map_nonneg`, `map_smul_of_tower`, `monotone'`, `nsmul_apply`, `toLinearMap_add`, `toLinearMap_inj`, `toLinearMap_injective`, `toLinearMap_nsmul`, `toLinearMap_zero`, `zero_apply`	18
Total	29

OrderHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofLinear` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `DFunLike.coe`	`OrderHomClass`	—	`of_addMonoidHom`
`of_addMonoidHom` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `DFunLike.coe`	`OrderHomClass`	—	`map_sub` `sub_nonneg`

PositiveLinearMap

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	2 math math: `add_apply`, `toLinearMap_add`
`instAddCommMonoid` 📖	CompOp	—
`instFunLike` 📖	CompOp	23 math math: `apply_le_of_isSelfAdjoint`, `coe_toLinearMap`, `nsmul_apply`, `preGNS_norm_def`, `map_nonneg`, `preGNS_inner_def`, `ext_iff`, `RealRMK.rieszMeasure_le_of_eq_one`, `RealRMK.integral_rieszMeasure`, `CompactlySupportedContinuousMap.toRealPositiveLinear_apply`, `exists_norm_apply_le`, `zero_apply`, `map_smul_of_tower`, `CompactlySupportedContinuousMap.toNNRealLinear_apply`, `add_apply`, `instLinearMapClass`, `instOrderHomClass`, `CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal`, `norm_apply_le_of_nonneg`, `CompactlySupportedContinuousMap.integralPositiveLinearMap_toFun`, `RealRMK.le_rieszMeasure_tsupport_subset`, `preGNS_norm_sq`, `map_isSelfAdjoint`
`instSMulNat` 📖	CompOp	2 math math: `nsmul_apply`, `toLinearMap_nsmul`
`instZero` 📖	CompOp	2 math math: `zero_apply`, `toLinearMap_zero`
`mk₀` 📖	CompOp	—
`toLinearMap` 📖	CompOp	7 math math: `monotone'`, `toLinearMap_inj`, `coe_toLinearMap`, `toLinearMap_injective`, `toLinearMap_zero`, `toLinearMap_nsmul`, `toLinearMap_add`
`toOrderHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `PositiveLinearMap` `instFunLike` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`coe_toLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `toLinearMap` `PositiveLinearMap` `instFunLike`	—	—
`ext` 📖	—	`DFunLike.coe` `PositiveLinearMap` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `PositiveLinearMap` `instFunLike`	—	`ext`
`instLinearMapClass` 📖	mathematical	—	`LinearMapClass` `PositiveLinearMap` `instFunLike`	—	`map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `LinearMap.map_smul'`
`instOrderHomClass` 📖	mathematical	—	`OrderHomClass` `PositiveLinearMap` `Preorder.toLE` `PartialOrder.toPreorder` `instFunLike`	—	`monotone'`
`map_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`DFunLike.coe` `PositiveLinearMap` `instFunLike`	—	`map_nonneg` `instOrderHomClass` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `instLinearMapClass`
`map_smul_of_tower` 📖	mathematical	—	`DFunLike.coe` `PositiveLinearMap` `instFunLike`	—	`LinearMapClass.map_smul_of_tower` `instLinearMapClass`
`monotone'` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.toAddHom` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap`	—	—
`nsmul_apply` 📖	mathematical	—	`DFunLike.coe` `PositiveLinearMap` `instFunLike` `instSMulNat` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	—
`toLinearMap_add` 📖	mathematical	—	`toLinearMap` `PositiveLinearMap` `instAdd` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instAdd`	—	—
`toLinearMap_inj` 📖	mathematical	—	`toLinearMap`	—	`toLinearMap_injective`
`toLinearMap_injective` 📖	mathematical	—	`PositiveLinearMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap`	—	`ext`
`toLinearMap_nsmul` 📖	mathematical	—	`toLinearMap` `PositiveLinearMap` `instSMulNat` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `LinearMap.addCommMonoid`	—	—
`toLinearMap_zero` 📖	mathematical	—	`toLinearMap` `PositiveLinearMap` `instZero` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instZero`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `PositiveLinearMap` `instFunLike` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—

PositiveLinearMapClass

Definitions

Name	Category	Theorems
`instCoeToLinearMap` 📖	CompOp	—
`toPositiveLinearMap` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`«term_→ₚ[_]_»` 📖	CompOp	—

---

← Back to Index