Commit 2023-07-16 12:56 08b081ea

chore(*): add mathlib4 synchronization comments (#19238) 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