chore(*): add mathlib4 synchronization comments

src/algebraic_topology/dold_kan/equivalence.lean

@@ -11,6 +11,9 @@ import algebraic_topology.dold_kan.normalized
 
 # The Dold-Kan correspondence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The Dold-Kan correspondence states that for any abelian category `A`, there is
 an equivalence between the category of simplicial objects in `A` and the
 category of chain complexes in `A` (with degrees indexed by `ℕ` and the

src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean

@@ -12,6 +12,9 @@ import category_theory.idempotents.simplicial_object
 
 # The Dold-Kan correspondence for pseudoabelian categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, for any idempotent complete additive category `C`,
 the Dold-Kan equivalence
 `idempotents.dold_kan.equivalence C : simplicial_object C ≌ chain_complex C ℕ`

src/combinatorics/quiver/covering.lean

@@ -11,6 +11,9 @@ import logic.equiv.basic
 /-!
 # Covering
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines coverings of quivers as prefunctors that are bijective on the
 so-called stars and costars at each vertex of the domain.
 

src/linear_algebra/quadratic_form/dual.lean

@@ -9,6 +9,9 @@ import linear_algebra.quadratic_form.prod
 /-!
 # Quadratic form structures related to `module.dual`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 * `bilin_form.dual_prod R M`, the bilinear form on `(f, x) : module.dual R M × M` defined as