Mathlib Changelog
v4
Changelog
About
Github
Theorem
ENNReal.nnreal_smul_lt_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_lt_top
View on Github →