chore(*): add mathlib4 synchronization comments

leanprover-community · Aug 29, 2023 · 41c0b18 · 41c0b18
1 parent ffde2d8
commit 41c0b18
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 0 deletions.
diff --git a/src/algebraic_topology/dold_kan/equivalence.lean b/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

diff --git a/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean b/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 ℕ`

diff --git a/src/combinatorics/quiver/covering.lean b/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.