Mathlib Changelog
v4
Changelog
About
Github
Def
Real.toEReal
Modification history
2025-03-16 19:16
Mathlib/Data/Real/EReal.lean
chore: stop conflating Option and WithTop in EReal (#22978)
Modified
Real.toEReal
View on Github →
2023-02-28 07:22
Mathlib/Data/Real/EReal.lean
feat: port Data.Real.EReal (#2501)
Added
Real.toEReal
View on Github →