Mathlib v3 is deprecated. Go to Mathlib v4

Def ennreal.of_nnreal_hom

Modification history

2022-03-11 23:40
src/data/real/ennreal.lean
chore(*): update to 3.41.0c (#12591)
Added ennreal.of_nnreal_homView on Github →
2021-10-23 20:04
src/data/real/ennreal.lean
chore(data/real): make more instances on real, nnreal, and ennreal computable (#9806) …
Deleted ennreal.of_nnreal_homView on Github →
2021-02-04 21:33
src/data/real/ennreal.lean
feat(data/real/ennreal): use notation for ennreal (#6044) …
Modified ennreal.of_nnreal_homView on Github →
2020-10-19 22:45
src/data/real/ennreal.lean
chore(topology/instances/ennreal): prove `nnreal.not_summable_iff_tendsto_nat_at_top` (#4670) …
Modified ennreal.of_nnreal_homView on Github →
2020-04-27 05:41
src/data/real/ennreal.lean
chore(data/real/*): use bundled homs to prove `coe_sum` etc (#2533)
Added ennreal.of_nnreal_homView on Github →