Commit 2023-11-07 14:42 bd3e369b

View on Github →

feat(Data/../ENNReal): add lemmas about ENNReal.ofReal (#8163) Compare ENNReal.ofReal r to Nat.cast n and literals.

<!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] -->

Open in
Gitpod

Estimated changes