Theorems · Definition · order theory
PositiveLinearMap.id
(R : Type u_1) →
(E₁ : Type u_2) →
[inst : Semiring R] →
[inst_1 : AddCommMonoid E₁] → [inst_2 : PartialOrder E₁] → [inst_3 : Module R E₁] → E₁ →ₚ[R] E₁The identity as a positive linear map.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idproof · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearMapproof · cited by 10,215
- PartialOrderstatement and proof · cited by 6,410
- OrderHomproof · cited by 934
- LinearMap.idproof · cited by 625
- PositiveLinearMapstatement · cited by 52
- OrderHom.idproof · cited by 37
Cited by5
Results whose statement or proof uses this declaration.
- PositiveLinearMap.comp_idstatement · cited by 0
- PositiveLinearMap.toLinearMap_idstatement and proof · cited by 0
- PositiveLinearMap.toOrderHom_idstatement · cited by 0
- PositiveLinearMap.id_applystatement and proof · cited by 0
- PositiveLinearMap.id_compstatement · cited by 0