Commit 2023-01-10 13:41 11c2b8c1
View on Github →chore(data/real/ennreal): Protect ambiguous lemmas (#18076)
Protect ennreal.X
if declaration X
already exists.
chore(data/real/ennreal): Protect ambiguous lemmas (#18076)
Protect ennreal.X
if declaration X
already exists.