Theorem NNReal.coeNNRealReal_zero

Modification history

2025-03-05 14:00
Mathlib/Topology/Instances/NNReal/Defs.lean
chore(Topology/Instances/*Real): organize instances by class (#22562) …
Modified NNReal.coeNNRealReal_zeroView on Github →
2025-02-14 21:47
Mathlib/Topology/Instances/NNReal/Defs.lean
chore: tidy various files (#21872)
Modified NNReal.coeNNRealReal_zeroView on Github →
2025-02-03 17:10
Mathlib/Topology/Instances/NNReal/Defs.lean
feat(Topology/ContinuousMap/CompactlySupported): turn a positive `Real`-linear functional into a `NNReal`-linear functional (#20257) …
Added NNReal.coeNNRealReal_zeroView on Github →