Theorem OrderHomClass.ofLinear

Modification history

2025-10-14 15:30

Mathlib/Algebra/Order/Module/PositiveLinearMap.lean

chore(Algebra/Order/Module/PositiveLinearMap): generalize `OrderHomClass.ofLinear` (#29626) …

Deleted OrderHomClass.ofLinear View on Github →

2025-05-03 14:10

Mathlib/Algebra/Order/Module/PositiveLinearMap.lean

feat(CStarAlgebra): define completely positive maps (#24359) …

Added OrderHomClass.ofLinear View on Github →