Def PositiveLinearMap.mk₀

Modification history

2025-04-10 16:38
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
chore: deprecate semibundled ordered algebraic typeclasses (#20676) …
Modified PositiveLinearMap.mk₀View on Github →
2025-03-30 03:51
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
feat(CStarAlgebra): define positive maps and show their continuity (#23210) …
Added PositiveLinearMap.mk₀View on Github →