Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.div_self

Modification history

2023-01-10 13:41

src/data/real/ennreal.lean

chore(data/real/ennreal): Protect ambiguous lemmas (#18076) …

Deleted ennreal.div_self View on Github →

2019-12-15 21:28

src/data/real/ennreal.lean

feat(data/real/ennreal): more lemmas, `*_cast` tags, use `lift` tactic (#1754) …

Modified ennreal.div_self View on Github →

2018-11-09 10:22

data/real/ennreal.lean

feat(analysis): add emetric spaces

Added ennreal.div_self View on Github →