mathlib3

08b63ab5 - chore(*): add mathlib4 synchronization comments (#19216)

chore(*): add mathlib4 synchronization comments (#19216) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Mon.colimits` * `algebra.category.fgModule.basic` * `analysis.complex.upper_half_plane.basic` * `analysis.inner_product_space.linear_pmap` * `analysis.special_functions.gamma.beta` * `analysis.special_functions.gamma.bohr_mollerup` * `analysis.special_functions.gaussian` * `category_theory.closed.ideal` * `category_theory.monoidal.Bimod` * `combinatorics.simple_graph.regularity.bound` * `combinatorics.simple_graph.regularity.chunk` * `combinatorics.simple_graph.regularity.increment` * `combinatorics.simple_graph.regularity.lemma` * `control.random` * `geometry.manifold.complex` * `geometry.manifold.mfderiv` * `geometry.manifold.partition_of_unity` * `linear_algebra.exterior_algebra.of_alternating` * `logic.equiv.array` * `number_theory.bertrand` * `number_theory.legendre_symbol.gauss_eisenstein_lemmas` * `number_theory.legendre_symbol.gauss_sum` * `number_theory.legendre_symbol.jacobi_symbol` * `number_theory.legendre_symbol.quadratic_char.gauss_sum` * `number_theory.legendre_symbol.quadratic_reciprocity` * `number_theory.sum_two_squares` * `number_theory.zsqrtd.quadratic_reciprocity` * `ring_theory.dedekind_domain.selmer_group` * `ring_theory.witt_vector.frobenius` * `ring_theory.witt_vector.identities` * `ring_theory.witt_vector.init_tail` * `ring_theory.witt_vector.verschiebung` * `set_theory.game.basic` * `set_theory.game.impartial` * `set_theory.game.ordinal` * `set_theory.surreal.basic` * `testing.slim_check.gen` * `testing.slim_check.sampleable` * `testing.slim_check.testable`