Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.mul_val

Modification history

2018-05-24 15:55
analysis/nnreal.lean
feat(analysis/ennreal): add further type class instances for nonnegative reals
Deleted nnreal.mul_valView on Github →
2018-05-24 15:55
analysis/nnreal.lean
feat(analysis/nnreal): define the nonnegative reals …
Added nnreal.mul_valView on Github →