Skip to content

Comments

[Merged by Bors] - chore: classify lemma was not necessary porting notes (category theory)#10674

Closed
pitmonticone wants to merge 6 commits intomasterfrom
pitmonticone/lemma-was-not-necessary
Closed

[Merged by Bors] - chore: classify lemma was not necessary porting notes (category theory)#10674
pitmonticone wants to merge 6 commits intomasterfrom
pitmonticone/lemma-was-not-necessary

Conversation

@pitmonticone
Copy link
Member

@pitmonticone pitmonticone commented Feb 17, 2024 •
edited by joelriou
Loading

Classifies by adding issue number (#10688) to porting notes claiming ext/simp lemma was not necessary.

@pitmonticone pitmonticone added awaiting-review easy < 20s of review time. See the lifecycle page for guidelines. porting-notes Mathlib3 to Mathlib4 porting notes. labels Feb 17, 2024
@pitmonticone pitmonticone added the t-category-theory Category theory label Feb 18, 2024
@pitmonticone pitmonticone changed the title chore: add issue number to lemma was not necessary porting notes chore: classify lemma was not necessary porting notes Feb 18, 2024
@pitmonticone pitmonticone changed the title chore: classify lemma was not necessary porting notes chore: classify lemma was not necessary porting notes (category theory) Feb 18, 2024
@joelriou
Copy link
Contributor

joelriou commented Feb 19, 2024

As these are simp or ext lemmas, I would think that it could be classified together with "added to ease automation" #10688 (cf. PR #10689 )

@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Feb 19, 2024
@pitmonticone
Copy link
Member Author

pitmonticone commented Feb 19, 2024 •
edited
Loading

Hi @joelriou, thank you for your review.

Could you please discuss your proposal here in order to reach a consensus?

@pitmonticone
Copy link
Member Author

pitmonticone commented Feb 19, 2024

@joelriou Done.

@joelriou
Copy link
Contributor

joelriou commented Feb 19, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Feb 19, 2024
@pitmonticone
chore: classify lemma was not necessary porting notes (category the…
964ad14 
…ory) (#10674)

Classifies by adding issue number (#10688) to porting notes claiming `ext/simp lemma was not necessary`.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 19, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Feb 19, 2024
@pitmonticone
chore: classify lemma was not necessary porting notes (category the…
f009681 
…ory) (#10674)

Classifies by adding issue number (#10688) to porting notes claiming `ext/simp lemma was not necessary`.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 19, 2024

Canceled.

@joelriou
Copy link
Contributor

joelriou commented Feb 19, 2024

Retrying...

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Feb 19, 2024
@pitmonticone @joelriou
chore: classify lemma was not necessary porting notes (category the…
6590f14 
…ory) (#10674)

Classifies by adding issue number (#10688) to porting notes claiming `ext/simp lemma was not necessary`.

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: classify lemma was not necessary porting notes (category theory) [Merged by Bors] - chore: classify lemma was not necessary porting notes (category theory) Feb 19, 2024
@mathlib-bors mathlib-bors bot closed this Feb 19, 2024
@mathlib-bors mathlib-bors bot deleted the pitmonticone/lemma-was-not-necessary branch February 19, 2024 21:11
thorimur pushed a commit that referenced this pull request Feb 24, 2024
@pitmonticone @joelriou @thorimur
chore: classify lemma was not necessary porting notes (category the…
9a1d2db 
…ory) (#10674)

Classifies by adding issue number (#10688) to porting notes claiming `ext/simp lemma was not necessary`.

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
thorimur pushed a commit that referenced this pull request Feb 26, 2024
@pitmonticone @joelriou @thorimur
chore: classify lemma was not necessary porting notes (category the…
16d789c 
…ory) (#10674)

Classifies by adding issue number (#10688) to porting notes claiming `ext/simp lemma was not necessary`.

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024
@pitmonticone @joelriou @riccardobrasca
chore: classify lemma was not necessary porting notes (category the…
25ae920 
…ory) (#10674)

Classifies by adding issue number (#10688) to porting notes claiming `ext/simp lemma was not necessary`.

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@pitmonticone @joelriou @dagurtomas
chore: classify lemma was not necessary porting notes (category the…
c8bfa56 
…ory) (#10674)

Classifies by adding issue number (#10688) to porting notes claiming `ext/simp lemma was not necessary`.

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

easy < 20s of review time. See the lifecycle page for guidelines. porting-notes Mathlib3 to Mathlib4 porting notes. ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@pitmonticone @joelriou