mathlib

d3e5621d - feat(data/real/ereal): add `ereal` := [-oo,oo] (#1703)

feat(data/real/ereal): add `ereal` := [-oo,oo] (#1703) * feat(data/real/ereal): add `ereal` := [-oo,oo] * some updates * some cleanup in ereal * move pattern attribute * works * more docstring * don't understand why this file was broken * more tidyup * deducing complete lattice from type class inference * another neg theorem * adding some module doc * tinkering * deriving addition Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>