Theorem NNReal.mk_one

Modification history

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