PR #19240 chore(*): add mathlib4 synchronization comments

chore(*): add mathlib4 synchronization comments #19240

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 6f4fe15c to 41c0b183 2 years ago

github-actions force pushed from 41c0b183 to f9282be1 2 years ago

github-actions force pushed from f9282be1 to 2e70f98a 2 years ago

github-actions force pushed from 2e70f98a to df1f954a 2 years ago

github-actions force pushed from df1f954a to 654d707e 2 years ago

YaelDillies removed review request 2 years ago

github-actions force pushed from 654d707e to d6d01bc2 2 years ago

github-actions force pushed from d6d01bc2 to 5ac49dd4 2 years ago

github-actions force pushed from 5ac49dd4 to 0c9b8973 2 years ago

github-actions force pushed from 0c9b8973 to 95aad471 2 years ago

github-actions force pushed from 95aad471 to 28da11e8 2 years ago

chore(*): add mathlib4 synchronization comments

949d67ea

github-actions force pushed from 28da11e8 to 949d67ea 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

easy awaiting-review mathlib4-synchronization

Milestone

No milestone