mathlib3

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

#19215

Closed