[Merged by Bors] - chore(*): add mathlib4 synchronization comments

src/algebra/lie/subalgebra.lean

@@ -9,6 +9,9 @@ import ring_theory.noetherian
 /-!
 # Lie subalgebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines Lie subalgebras of a Lie algebra and provides basic related definitions and
 results.
 

src/category_theory/limits/shapes/kernel_pair.lean

@@ -10,6 +10,9 @@ import category_theory.limits.shapes.regular_mono
 /-!
 # Kernel pairs
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines what it means for a parallel pair of morphisms `a b : R ⟶ X` to be the kernel pair
 for a morphism `f`.
 Some properties of kernel pairs are given, namely allowing one to transfer between

src/category_theory/monoidal/preadditive.lean

@@ -9,6 +9,9 @@ import category_theory.monoidal.functor
 /-!
 # Preadditive monoidal categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A monoidal category is `monoidal_preadditive` if it is preadditive and tensor product of morphisms
 is linear in both factors.
 -/

src/category_theory/preadditive/single_obj.lean

@@ -9,6 +9,9 @@ import category_theory.single_obj
 /-!
 # `single_obj α` is preadditive when `α` is a ring.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 namespace category_theory

src/linear_algebra/sesquilinear_form.lean

@@ -12,6 +12,9 @@ import ring_theory.non_zero_divisors
 /-!
 # Sesquilinear form
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This files provides properties about sesquilinear forms. The maps considered are of the form
 `M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R`, where `I₁ : R₁ →+* R` and `I₂ : R₂ →+* R` are ring homomorphisms and
 `M₁` is a module over `R₁` and `M₂` is a module over `R₂`.

src/number_theory/padics/padic_val.lean

@@ -10,6 +10,9 @@ import tactic.ring_exp
 /-!
 # p-adic Valuation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the `p`-adic valuation on `ℕ`, `ℤ`, and `ℚ`.
 
 The `p`-adic valuation on `ℚ` is the difference of the multiplicities of `p` in the numerator and

src/ring_theory/localization/fraction_ring.lean

@@ -9,6 +9,9 @@ import ring_theory.localization.basic
 /-!
 # Fraction ring / fraction field Frac(R) as localization
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
  * `is_fraction_ring R K` expresses that `K` is a field of fractions of `R`, as an abbreviation of

src/topology/algebra/uniform_ring.lean

@@ -10,6 +10,9 @@ import topology.algebra.ring.ideal
 /-!
 # Completion of topological rings:
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This files endows the completion of a topological ring with a ring structure.
 More precisely the instance `uniform_space.completion.ring` builds a ring structure
 on the completion of a ring endowed with a compatible uniform structure in the sense of

src/topology/covering.lean

@@ -9,6 +9,9 @@ import topology.fiber_bundle.basic
 /-!
 # Covering Maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines covering maps.
 
 ## Main definitions

src/topology/fiber_bundle/basic.lean

@@ -8,6 +8,9 @@ import topology.fiber_bundle.trivialization
 /-!
 # Fiber bundles
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Mathematically, a (topological) fiber bundle with fiber `F` over a base `B` is a space projecting on
 `B` for which the fibers are all homeomorphic to `F`, such that the local situation around each
 point is a direct product.