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

[github-actions[bot]]

Regenerated from the port status wiki page. Relates to the following files:

• algebra.expr
• algebraic_geometry.morphisms.finite_type
• algebraic_geometry.morphisms.ring_hom_properties
• arithcc
• canonically_ordered_comm_semiring_two_mul
• char_p_zero_ne_char_zero
• cyclotomic_105
• data.matrix.auto
• direct_sum_is_internal
• examples.mersenne_primes
• examples.prop_encodable
• geometry.manifold.instances.sphere
• girard
• homogeneous_prime_not_prime
• imo.imo1959_q1
• imo.imo1960_q1
• imo.imo1962_q1
• imo.imo1962_q4
• imo.imo1964_q1
• imo.imo1969_q1
• imo.imo1972_q5
• imo.imo1975_q1
• imo.imo1977_q6
• imo.imo1981_q3
• imo.imo1987_q1
• imo.imo1988_q6
• imo.imo1994_q1
• imo.imo1998_q2
• imo.imo2001_q2
• imo.imo2001_q6
• imo.imo2005_q3
• imo.imo2005_q4
• imo.imo2006_q3
• imo.imo2006_q5
• imo.imo2008_q2
• imo.imo2008_q3
• imo.imo2008_q4
• imo.imo2011_q3
• imo.imo2011_q5
• imo.imo2013_q1
• imo.imo2013_q5
• imo.imo2019_q1
• imo.imo2019_q2
• imo.imo2019_q4
• imo.imo2020_q2
• imo.imo2021_q1
• linear_order_with_pos_mul_pos_eq_zero
• map_floor
• miu_language.basic
• miu_language.decision_nec
• miu_language.decision_suf
• oxford_invariants.2021summer.week3_p1
• phillips
• pseudoelement
• quadratic_form
• seminorm_lattice_not_distrib
• sensitivity
• sorgenfrey_line
• wiedijk_100_theorems.abel_ruffini
• wiedijk_100_theorems.area_of_a_circle
• wiedijk_100_theorems.ascending_descending_sequences
• wiedijk_100_theorems.ballot_problem
• wiedijk_100_theorems.birthday_problem
• wiedijk_100_theorems.cubing_a_cube
• wiedijk_100_theorems.friendship_graphs
• wiedijk_100_theorems.herons_formula
• wiedijk_100_theorems.inverse_triangle_sum
• wiedijk_100_theorems.konigsberg
• wiedijk_100_theorems.partition
• wiedijk_100_theorems.perfect_numbers
• wiedijk_100_theorems.solution_of_cubic
• wiedijk_100_theorems.sum_of_prime_reciprocals_diverges
• zero_divisors_in_add_monoid_algebras

---

The following files have no module docstring, so I have not added a message in this PR

• control.basic
• control.monad.cont
• control.monad.writer
• control.traversable.derive
• data.array.lemmas
• data.bitvec.basic
• data.buffer.basic
• data.rbmap.basic
• data.rbmap.default
• data.rbtree.basic
• data.rbtree.default_lt
• data.rbtree.find
• data.rbtree.init
• data.rbtree.insert
• data.rbtree.main
• data.rbtree.min_max
• data.seq.computation
• data.seq.parallel
• data.seq.seq
• data.seq.wseq

Please make a PR to add a module docstring (for Lean3 and Lean4!), then I will add the freeze comment next time.

---

The following files no longer exist in Lean 3' mathlib, so I have not added a message in this PR

• data.buffer.parser
• data.dlist
• data.vector
• init.algebra.classes
• init.algebra.functions
• init.algebra.order
• init.control.lawful
• init.data.int.bitwise
• init.data.int.comp_lemmas
• init.data.list.instances
• init.data.nat.bitwise
• init.data.nat.gcd
• init.data.nat.lemmas
• init.data.ordering.lemmas
• init.data.subtype.basic
• init.function
• init.ite_simp
• init.meta.well_founded_tactics

In future we should find where they moved to, and check that the files are still in sync.

---

I am a bot; please check that I have not put a comment in a bad place before running bors merge!

[eric-wieser]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests