Theorem ENNReal.nnreal_smul_ne_top

Modification history

2024-08-31 13:47
Mathlib/Data/ENNReal/Operations.lean
feat(ENNReal): Scalar multiplication by `NNReal` is finite (#16319) …
Added ENNReal.nnreal_smul_ne_topView on Github →