Theorem OrderHomClass.of_addMonoidHom

Modification history

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 →