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

Closed

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

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 5a951413 to 94458c7f 2 years ago

github-actions requested a review 2 years ago

github-actions force pushed from 94458c7f to 23bb1b90 2 years ago

github-actions force pushed from 23bb1b90 to 4fd3a0ae 2 years ago

github-actions requested a review 2 years ago

github-actions force pushed from 4fd3a0ae to a852124e 2 years ago

chore(*): add mathlib4 synchronization comments

cae80189

github-actions force pushed from a852124e to cae80189 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 #19231 Closed

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

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

Closed