mathlib3
11c2b8c1 - chore(data/real/ennreal): Protect ambiguous lemmas (#18076)

Commit
3 years ago
chore(data/real/ennreal): Protect ambiguous lemmas (#18076) Protect `ennreal.X` if declaration `X` already exists.
Author
Parents
Loading