Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-26 06:46 21d8e0af

View on Github →

chore(data/real/ennreal): +2 simple lemmas (#2539) Extracted from #2311

Estimated changes