Commit 2023-03-13 06:41 69c6a5a1

chore(*): add mathlib4 synchronization comments (#18566) Regenerated from the port status wiki page. Relates to the following files:

• algebra.algebra.subalgebra.basic
• algebra.algebra.subalgebra.tower
• algebra.free_non_unital_non_assoc_algebra
• algebra.monoid_algebra.basic
• algebra.monoid_algebra.support
• algebra.polynomial.big_operators
• algebra.star.subalgebra
• analysis.normed.group.ball_sphere
• analysis.normed.group.basic
• analysis.normed.group.completion
• analysis.normed.group.hom
• analysis.normed.group.hom_completion
• analysis.normed.group.infinite_sum
• analysis.normed.group.seminorm
• analysis.normed_space.indicator_function
• analysis.subadditive
• category_theory.abelian.images
• category_theory.abelian.non_preadditive
• category_theory.adjunction.comma
• category_theory.concrete_category.reflects_isomorphisms
• category_theory.is_connected
• category_theory.limits.bicones
• category_theory.limits.comma
• category_theory.limits.cone_category
• category_theory.limits.constructions.equalizers
• category_theory.limits.constructions.finite_products_of_binary_products
• category_theory.limits.constructions.limits_of_products_and_equalizers
• category_theory.limits.essentially_small
• category_theory.limits.kan_extension
• category_theory.limits.lattice
• category_theory.limits.mono_coprod
• category_theory.limits.opposites
• category_theory.limits.preserves.filtered
• category_theory.limits.preserves.shapes.biproducts
• category_theory.limits.preserves.shapes.zero
• category_theory.limits.shapes.biproducts
• category_theory.limits.shapes.finite_products
• category_theory.limits.shapes.functor_category
• category_theory.limits.shapes.kernels
• category_theory.limits.shapes.normal_mono.basic
• category_theory.limits.shapes.normal_mono.equalizers
• category_theory.limits.shapes.zero_morphisms
• category_theory.limits.small_complete
• category_theory.limits.types
• category_theory.linear.basic
• category_theory.linear.functor_category
• category_theory.monoidal.End
• category_theory.preadditive.additive_functor
• category_theory.preadditive.basic
• category_theory.preadditive.biproducts
• category_theory.preadditive.functor_category
• combinatorics.hindman
• control.bifunctor
• control.bitraversable.basic
• data.complex.basic
• data.nat.choose.cast
• data.nat.choose.vandermonde
• data.nat.factorial.cast
• data.polynomial.basic
• data.polynomial.cardinal
• data.polynomial.coeff
• data.polynomial.degree.definitions
• data.polynomial.degree.lemmas
• data.polynomial.degree.trailing_degree
• data.polynomial.derivative
• data.polynomial.erase_lead
• data.polynomial.eval
• data.polynomial.induction
• data.polynomial.inductions
• data.polynomial.monic
• data.polynomial.monomial
• data.polynomial.reverse
• data.real.sqrt
• data.tree
• linear_algebra.affine_space.slope
• logic.equiv.functor
• number_theory.basic
• order.jordan_holder
• ring_theory.adjoin.basic
• ring_theory.ideal.operations
• ring_theory.ideal.quotient
• ring_theory.localization.basic
• ring_theory.nilpotent
• ring_theory.polynomial.pochhammer
• topology.algebra.affine
• topology.algebra.localization
• topology.algebra.ring.ideal
• topology.fiber_bundle.trivialization
• topology.instances.ennreal
• topology.metric_space.completion
• topology.metric_space.gluing
• topology.metric_space.isometric_smul
• topology.metric_space.isometry
• topology.uniform_space.compare_reals
• topology.unit_interval