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

Closed

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

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 5bf7ebbf to a4ab5f7d 2 years ago

github-actions force pushed from a4ab5f7d to 3225789a 2 years ago

github-actions force pushed from 3225789a to 856b893a 2 years ago

github-actions requested a review 2 years ago

chore(*): add mathlib4 synchronization comments

de0e1c6f

github-actions force pushed from 856b893a to de0e1c6f 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

Milestone

No milestone

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

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

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

Closed