mathlib3
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19238

Closed

[Merged by Bors] - chore(*): add mathlib4 synchronization comments #19238

github-actions wants to merge 1 commit into master from create-pull-request/patch

github-actions requested a review 2 years ago

github-actions added awaiting-review

github-actions added easy

github-actions added mathlib4-synchronization

github-actions force pushed from a4756722 to e1589b7a 2 years ago

kim-em added not-too-late

chore(*): add mathlib4 synchronization comments

43b242f7

github-actions force pushed from e1589b7a to 43b242f7 2 years ago

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~chore(*): add mathlib4 synchronization comments~~ [Merged by Bors] - chore(*): add mathlib4 synchronization comments 2 years ago

bors closed this 2 years ago

bors deleted the create-pull-request/patch branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge easy mathlib4-synchronization not-too-late

Milestone

No milestone

mathlib3 [Merged by Bors] - chore(*): add mathlib4 synchronization comments #19238 Closed

[Merged by Bors] - chore(*): add mathlib4 synchronization comments #19238

mathlib3
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19238

Closed