Commit 2026-06-13 14:25 f1ceb733

View on Github →

feat: clean up PositiveLinearMap and add API (#40492) Among other things, this removes the coercion from the morphism class into the morphism type, and renames the underlying convenience constructor to PositiveLinearMap.ofClass.

Estimated changes

Modified Mathlib/Algebra/Order/Module/PositiveLinearMap.lean

modified theorem OrderHomClass.of_addMonoidHom

added def PositiveLinearMap.comp

added theorem PositiveLinearMap.comp_id

added theorem PositiveLinearMap.id_comp

added def PositiveLinearMap.ofClass

added theorem PositiveLinearMap.toOrderHom_comp

added theorem PositiveLinearMap.toOrderHom_id

deleted def PositiveLinearMapClass.toPositiveLinearMap

Modified Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean