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

Closed

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

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

github-actions added awaiting-review

github-actions added easy

github-actions added mathlib4-synchronization

chore(*): add mathlib4 synchronization comments

ec32183a

github-actions force pushed from 4c307e71 to ec32183a 3 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 3 years ago

bors closed this 3 years ago

bors deleted the create-pull-request/patch branch 3 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 #19239 Closed

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

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

Closed