Skip to content

[Merged by Bors] - feat: missing nnratCast lemmas for RCLike#39620

Closed
eric-wieser wants to merge 2 commits into
leanprover-community:masterfrom
eric-wieser:ofReal_nnratCast
Closed

[Merged by Bors] - feat: missing nnratCast lemmas for RCLike#39620
eric-wieser wants to merge 2 commits into
leanprover-community:masterfrom
eric-wieser:ofReal_nnratCast

Conversation

@eric-wieser

@eric-wieser eric-wieser commented May 20, 2026

Copy link
Copy Markdown
Member

Open in Gitpod

@eric-wieser @Whysoserioushah
feat: missing nnratCast lemmas for RCLike
0edbd40 
Co-authored-by: Whysoserioushah <yx3021@ic.ac.uk>
@eric-wieser eric-wieser added the easy < 20s of review time. See the lifecycle page for guidelines. label May 20, 2026
@eric-wieser eric-wieser mentioned this pull request May 20, 2026
Open
@github-actions

github-actions Bot commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 150dde15d9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ nnratCast_im
+ nnratCast_re

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added the t-analysis Analysis (normed *, calculus) label May 20, 2026
Whysoserioushah
Whysoserioushah approved these changes May 20, 2026
View reviewed changes

@Whysoserioushah Whysoserioushah left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

Comment thread Mathlib/Analysis/RCLike/Basic.lean
@eric-wieser eric-wieser mentioned this pull request May 20, 2026
Closed
ocfnash
ocfnash approved these changes May 25, 2026
View reviewed changes

@ocfnash ocfnash left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors merge

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 25, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 25, 2026
@eric-wieser
feat: missing nnratCast lemmas for RCLike (#39620)
773df06
@mathlib-bors

mathlib-bors Bot commented May 25, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat: missing nnratCast lemmas for RCLike [Merged by Bors] - feat: missing nnratCast lemmas for RCLike May 25, 2026
@mathlib-bors mathlib-bors Bot closed this May 25, 2026
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@eric-wieser @b-mehta
feat: missing nnratCast lemmas for RCLike (leanprover-community#39620)
add09cb
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@eric-wieser @Bergschaf
feat: missing nnratCast lemmas for RCLike (leanprover-community#39620)
a2e3b88
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ocfnash ocfnash ocfnash approved these changes
+1 more reviewer
@Whysoserioushah Whysoserioushah Whysoserioushah approved these changes
Reviewers whose approvals may not affect merge requirements

Assignees

@j-loreaux j-loreaux

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@eric-wieser @ocfnash @Whysoserioushah @j-loreaux