chore(*): add mathlib4 synchronization comments (#17686)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: https://github.com/leanprover-community/mathlib4/pull/661
* `algebra.group.inj_surj`: https://github.com/leanprover-community/mathlib4/pull/707
* `algebra.group.order_synonym`: https://github.com/leanprover-community/mathlib4/pull/651
* `algebra.group.units`: https://github.com/leanprover-community/mathlib4/pull/549
* `algebra.hierarchy_design`: https://github.com/leanprover-community/mathlib4/pull/657
* `algebra.opposites`: https://github.com/leanprover-community/mathlib4/pull/644
* `algebra.quotient`: https://github.com/leanprover-community/mathlib4/pull/643
* `algebra.ring.defs`: https://github.com/leanprover-community/mathlib4/pull/655
* `algebra.ring.order_synonym`: https://github.com/leanprover-community/mathlib4/pull/671
* `control.equiv_functor`: https://github.com/leanprover-community/mathlib4/pull/649
* `data.dlist.basic`: https://github.com/leanprover-community/mathlib4/pull/616
* `data.int.cast.basic`: https://github.com/leanprover-community/mathlib4/pull/670
* `data.lazy_list`: https://github.com/leanprover-community/mathlib4/pull/686
* `data.list.lex`: https://github.com/leanprover-community/mathlib4/pull/672
* `data.option.n_ary`: https://github.com/leanprover-community/mathlib4/pull/656
* `data.sigma.lex`: https://github.com/leanprover-community/mathlib4/pull/646
* `data.ulift`: https://github.com/leanprover-community/mathlib4/pull/703
* `group_theory.eckmann_hilton`: https://github.com/leanprover-community/mathlib4/pull/626
* `logic.equiv.basic`: https://github.com/leanprover-community/mathlib4/pull/631
* `order.iterate`: https://github.com/leanprover-community/mathlib4/pull/648
