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

Closed

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

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

chore(*): add mathlib4 synchronization comments

46d60346

github-actions requested a review 2 years ago

github-actions added awaiting-review

github-actions added easy

github-actions added mathlib4-synchronization

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

Milestone

No milestone

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

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

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

Closed