Skip to content

[Merged by Bors] - chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now#8496

Closed
dwrensha wants to merge 1 commit intomasterfrom
imo-1994q1-porting-note
Closed

[Merged by Bors] - chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now#8496
dwrensha wants to merge 1 commit intomasterfrom
imo-1994q1-porting-note

Conversation

@dwrensha
Copy link
Copy Markdown
Member

@dwrensha dwrensha commented Nov 18, 2023

According to git bisect, #7905 is what made the single linarith call work here.


Open in Gitpod

@dwrensha dwrensha changed the title chore: address porting note in Imo1994Q1 -- linarith works now chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now Nov 18, 2023
@dwrensha dwrensha added the easy < 20s of review time. See the lifecycle page for guidelines. label Nov 18, 2023
@riccardobrasca
Copy link
Copy Markdown
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 19, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 19, 2023
…s now (#8496)

According to `git bisect`, #7905 is what made the single `linarith` call work here.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 19, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now [Merged by Bors] - chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now Nov 19, 2023
@mathlib-bors mathlib-bors bot closed this Nov 19, 2023
@mathlib-bors mathlib-bors bot deleted the imo-1994q1-porting-note branch November 19, 2023 11:09
alexkeizer pushed a commit that referenced this pull request Nov 21, 2023
…s now (#8496)

According to `git bisect`, #7905 is what made the single `linarith` call work here.
grunweg pushed a commit that referenced this pull request Dec 15, 2023
…s now (#8496)

According to `git bisect`, #7905 is what made the single `linarith` call work here.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants