Def PositiveLinearMapClass.toPositiveLinearMap

Modification history

2026-06-13 14:25
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
feat: clean up `PositiveLinearMap` and add API (#40492) …
Deleted PositiveLinearMapClass.toPositiveLinearMapView on Github →
2025-03-30 03:51
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
feat(CStarAlgebra): define positive maps and show their continuity (#23210) …
Added PositiveLinearMapClass.toPositiveLinearMapView on Github →