Commit 2023-02-24 11:52 b2ff9a3d
View on Github →chore(data/real/nnreal): drop some lemmas (#18492)
These lemmas are now available for any semifield, so we don't need them.
All these lemmas are @[deprecated] in the Mathlib 4 port and will be removed in the forward-port of this PR.