Commit 2025-10-14 15:30 4e6ecfb5

View on Github →

chore(Algebra/Order/Module/PositiveLinearMap): generalize OrderHomClass.ofLinear (#29626) Generalize OrderHomClass.ofLinear from linear maps to additive group homomorphisms.

Estimated changes

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

deleted theorem OrderHomClass.ofLinear

added theorem OrderHomClass.of_addMonoidHom

Modified Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean