2025-02-03 17:10
Mathlib/Topology/ContinuousMap/CompactlySupported.lean
feat(Topology/ContinuousMap/CompactlySupported): turn a positive `Real`-linear functional into a `NNReal`-linear functional (#20257) …
Added CompactlySupportedContinuousMap.coe_toRealLinearMap