Theorem PositiveLinearMap.ext

Modification history

2025-08-21 17:58
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
refactor(MeasureTheory/RieszMarkovKakutani): Use PositiveLinearMap (#28059) …
Added PositiveLinearMap.extView on Github →