Theorem ENNReal.coe_nnratCast

Modification history

2025-01-21 01:50
Mathlib/Data/ENNReal/Basic.lean
fix: make `NNRatCast` computable for `NNReal` and `ENNReal` (#20884) …
Added ENNReal.coe_nnratCastView on Github →