Theorem OrderHomClass.of_addMonoidHom

Modification history

2026-06-13 14:25
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
feat: clean up `PositiveLinearMap` and add API (#40492) …
Modified OrderHomClass.of_addMonoidHomView on Github →
2025-10-14 15:30
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
chore(Algebra/Order/Module/PositiveLinearMap): generalize `OrderHomClass.ofLinear` (#29626) …
Added OrderHomClass.of_addMonoidHomView on Github →