chore(*): add mathlib4 synchronization comments (#19063)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.algebraic_card`
* `algebra.category.GroupWithZero`
* `algebra.category.Ring.instances`
* `algebra.dual_quaternion`
* `algebra.quaternion`
* `algebra.quaternion_basis`
* `analysis.calculus.fderiv.add`
* `analysis.calculus.fderiv.comp`
* `analysis.calculus.fderiv.equiv`
* `analysis.calculus.fderiv.linear`
* `analysis.calculus.fderiv.prod`
* `analysis.calculus.fderiv.restrict_scalars`
* `analysis.convex.between`
* `analysis.convex.strict_convex_between`
* `analysis.locally_convex.strong_topology`
* `combinatorics.configuration`
* `data.real.irrational`
* `dynamics.ergodic.conservative`
* `field_theory.minpoly.basic`
* `field_theory.minpoly.field`
* `group_theory.perm.cycle.concrete`
* `linear_algebra.bilinear_form`
* `linear_algebra.bilinear_form.tensor_product`
* `linear_algebra.coevaluation`
* `linear_algebra.contraction`
* `linear_algebra.dual`
* `linear_algebra.matrix.dual`
* `measure_theory.constructions.borel_space.metrizable`
* `measure_theory.covering.vitali`
* `measure_theory.function.special_functions.is_R_or_C`
* `measure_theory.integral.lebesgue_normed_space`
* `measure_theory.integral.riesz_markov_kakutani`
* `measure_theory.measure.content`
* `measure_theory.measure.giry_monad`
* `number_theory.legendre_symbol.zmod_char`
* `number_theory.padics.padic_numbers`
* `order.interval`
* `ring_theory.algebraic`
* `ring_theory.artinian`
* `ring_theory.discrete_valuation_ring.basic`
* `ring_theory.graded_algebra.radical`
* `ring_theory.integral_closure`
* `ring_theory.localization.as_subring`
* `ring_theory.localization.away.basic`
* `ring_theory.localization.cardinality`
* `ring_theory.localization.localization_localization`
* `ring_theory.power_series.basic`
* `ring_theory.power_series.well_known`
* `ring_theory.witt_vector.witt_polynomial`
* `topology.metric_space.metrizable`
* `topology.metric_space.thickened_indicator`
* `topology.sheaves.punit`
* `topology.urysohns_bounded`
* `topology.vector_bundle.basic`
* `topology.vector_bundle.constructions`
