Theorem PositiveLinearMap.comp_id

Modification history

2026-06-13 14:25
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
feat: clean up `PositiveLinearMap` and add API (#40492) …
Added PositiveLinearMap.comp_idView on Github →