Def ENNReal.toNNRealHom

Modification history

2026-02-17 23:08
Mathlib/Data/ENNReal/Real.lean
chore: bump toolchain to v4.29.0-rc1 (#35459)
Deleted ENNReal.toNNRealHomView on Github →
2025-03-12 23:13
Mathlib/Data/ENNReal/Real.lean
chore(Data/(E)(NN)Real): address porting notes (#22883) …
Modified ENNReal.toNNRealHomView on Github →
2024-01-25 21:01
Mathlib/Data/ENNReal/Basic.lean
chore(Data/ENNReal/Basic): split file (#9869)
Modified ENNReal.toNNRealHomView on Github →
2023-02-27 08:10
Mathlib/Data/Real/ENNReal.lean
feat: port Data.Real.ENNReal (#2388) …
Added ENNReal.toNNRealHomView on Github →