chore(*): add mathlib4 synchronization comments (#19196)

github-actions[bot] · github-actions[bot] · commit 2a0ce625dbb0 · 2023-06-17T06:21:17.000Z
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.BoolRing` * `algebra.continued_fractions.computation.approximation_corollaries` * `category_theory.monoidal.internal.functor_category` * `field_theory.galois` * `field_theory.minpoly.is_integrally_closed` * `field_theory.primitive_element` * `linear_algebra.matrix.ldl` * `number_theory.diophantine_approximation` * `number_theory.pell` * `number_theory.primes_congruent_one` * `order.category.FinBoolAlg` * `probability.kernel.composition` * `probability.kernel.cond_cdf` * `probability.kernel.invariance` * `ring_theory.polynomial.cyclotomic.eval` * `ring_theory.polynomial.cyclotomic.expand` * `ring_theory.polynomial.cyclotomic.roots` * `ring_theory.polynomial.gauss_lemma` * `ring_theory.polynomial.selmer` * `ring_theory.ring_hom.finite_type` * `ring_theory.roots_of_unity.minpoly` * `topology.category.UniformSpace` * `topology.continuous_function.zero_at_infty` * `topology.sheaves.operations`
diff --git a/src/algebra/category/BoolRing.lean b/src/algebra/category/BoolRing.lean
@@ -10,6 +10,9 @@ import order.category.BoolAlg
 /-!
 # The category of Boolean rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `BoolRing`, the category of Boolean rings.
 
 ## TODO
diff --git a/src/algebra/continued_fractions/computation/approximation_corollaries.lean b/src/algebra/continued_fractions/computation/approximation_corollaries.lean
@@ -12,6 +12,9 @@ import topology.order.basic
 /-!
 # Corollaries From Approximation Lemmas (`algebra.continued_fractions.computation.approximations`)
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Summary
 
 We show that the generalized_continued_fraction given by `generalized_continued_fraction.of` in fact
diff --git a/src/category_theory/monoidal/internal/functor_category.lean b/src/category_theory/monoidal/internal/functor_category.lean
@@ -9,6 +9,9 @@ import category_theory.monoidal.functor_category
 /-!
 # `Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When `D` is a monoidal category,
 monoid objects in `C ⥤ D` are the same thing as functors from `C` into the monoid objects of `D`.
 
diff --git a/src/field_theory/galois.lean b/src/field_theory/galois.lean
@@ -11,6 +11,9 @@ import group_theory.group_action.fixing_subgroup
 /-!
 # Galois Extensions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define Galois extensions as extensions which are both separable and normal.
 
 ## Main definitions
diff --git a/src/field_theory/minpoly/is_integrally_closed.lean b/src/field_theory/minpoly/is_integrally_closed.lean
@@ -10,6 +10,9 @@ import ring_theory.polynomial.gauss_lemma
 /-!
 # Minimal polynomials over a GCD monoid
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file specializes the theory of minpoly to the case of an algebra over a GCD monoid.
 
 ## Main results
diff --git a/src/field_theory/primitive_element.lean b/src/field_theory/primitive_element.lean
@@ -12,6 +12,9 @@ import ring_theory.integral_domain
 /-!
 # Primitive Element Theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the primitive element theorem.
 
 ## Main results
diff --git a/src/linear_algebra/matrix/ldl.lean b/src/linear_algebra/matrix/ldl.lean
@@ -8,6 +8,9 @@ import linear_algebra.matrix.pos_def
 
 /-! # LDL decomposition
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the LDL-decomposition of matricies: Any positive definite matrix `S` can be
 decomposed as `S = LDLᴴ` where `L` is a lower-triangular matrix and `D` is a diagonal matrix.
 
diff --git a/src/number_theory/diophantine_approximation.lean b/src/number_theory/diophantine_approximation.lean
@@ -14,6 +14,9 @@ import tactic.basic
 /-!
 # Diophantine Approximation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The first part of this file gives proofs of various versions of
 **Dirichlet's approximation theorem** and its important consequence that when $\xi$ is an
 irrational real number, then there are infinitely many rationals $x/y$ (in lowest terms)
diff --git a/src/number_theory/pell.lean b/src/number_theory/pell.lean
@@ -12,6 +12,9 @@ import number_theory.zsqrtd.basic
 /-!
 # Pell's Equation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 *Pell's Equation* is the equation $x^2 - d y^2 = 1$, where $d$ is a positive integer
 that is not a square, and one is interested in solutions in integers $x$ and $y$.
 
diff --git a/src/number_theory/primes_congruent_one.lean b/src/number_theory/primes_congruent_one.lean
@@ -9,6 +9,9 @@ import ring_theory.polynomial.cyclotomic.eval
 /-!
 # Primes congruent to one
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove that, for any positive `k : ℕ`, there are infinitely many primes `p` such that
 `p ≡ 1 [MOD k]`.
 -/
diff --git a/src/order/category/FinBoolAlg.lean b/src/order/category/FinBoolAlg.lean
@@ -11,6 +11,9 @@ import order.hom.complete_lattice
 /-!
 # The category of finite boolean algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `FinBoolAlg`, the category of finite boolean algebras.
 
 ## TODO
diff --git a/src/probability/kernel/composition.lean b/src/probability/kernel/composition.lean
@@ -9,6 +9,9 @@ import probability.kernel.measurable_integral
 /-!
 # Product and composition of kernels
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define
 * the composition-product `κ ⊗ₖ η` of two s-finite kernels `κ : kernel α β` and
   `η : kernel (α × β) γ`, a kernel from `α` to `β × γ`.
diff --git a/src/probability/kernel/cond_cdf.lean b/src/probability/kernel/cond_cdf.lean
@@ -10,6 +10,9 @@ import measure_theory.decomposition.radon_nikodym
 /-!
 # Conditional cumulative distribution function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given `ρ : measure (α × ℝ)`, we define the conditional cumulative distribution function
 (conditional cdf) of `ρ`. It is a function `cond_cdf ρ : α → ℝ → ℝ` such that if `ρ` is a finite
 measure, then for all `a : α` `cond_cdf ρ a` is monotone and right-continuous with limit 0 at -∞
diff --git a/src/probability/kernel/invariance.lean b/src/probability/kernel/invariance.lean
@@ -8,6 +8,9 @@ import probability.kernel.composition
 /-!
 # Invariance of measures along a kernel
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We say that a measure `μ` is invariant with respect to a kernel `κ` if its push-forward along the
 kernel `μ.bind κ` is the same measure.
 
diff --git a/src/ring_theory/polynomial/cyclotomic/eval.lean b/src/ring_theory/polynomial/cyclotomic/eval.lean
@@ -12,6 +12,9 @@ import analysis.complex.arg
 
 /-!
 # Evaluating cyclotomic polynomials
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 This file states some results about evaluating cyclotomic polynomials in various different ways.
 ## Main definitions
 * `polynomial.eval(₂)_one_cyclotomic_prime(_pow)`: `eval 1 (cyclotomic p^k R) = p`.
diff --git a/src/ring_theory/polynomial/cyclotomic/expand.lean b/src/ring_theory/polynomial/cyclotomic/expand.lean
@@ -9,6 +9,9 @@ import ring_theory.polynomial.cyclotomic.roots
 /-!
 # Cyclotomic polynomials and `expand`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We gather results relating cyclotomic polynomials and `expand`.
 
 ## Main results
diff --git a/src/ring_theory/polynomial/cyclotomic/roots.lean b/src/ring_theory/polynomial/cyclotomic/roots.lean
@@ -10,6 +10,9 @@ import ring_theory.roots_of_unity.minpoly
 /-!
 # Roots of cyclotomic polynomials.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We gather results about roots of cyclotomic polynomials. In particular we show in
 `polynomial.cyclotomic_eq_minpoly` that `cyclotomic n R` is the minimal polynomial of a primitive
 root of unity.
diff --git a/src/ring_theory/polynomial/gauss_lemma.lean b/src/ring_theory/polynomial/gauss_lemma.lean
@@ -12,6 +12,9 @@ import ring_theory.integrally_closed
 /-!
 # Gauss's Lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Gauss's Lemma is one of a few results pertaining to irreducibility of primitive polynomials.
 
 ## Main Results
diff --git a/src/ring_theory/polynomial/selmer.lean b/src/ring_theory/polynomial/selmer.lean
@@ -11,6 +11,9 @@ import tactic.linear_combination
 /-!
 # Irreducibility of Selmer Polynomials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves irreducibility of the Selmer polynomials `X ^ n - X - 1`.
 
 ## Main results
diff --git a/src/ring_theory/ring_hom/finite_type.lean b/src/ring_theory/ring_hom/finite_type.lean
@@ -10,6 +10,9 @@ import ring_theory.localization.inv_submonoid
 
 # The meta properties of finite-type ring homomorphisms.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The main result is `ring_hom.finite_is_local`.
 
 -/
diff --git a/src/ring_theory/roots_of_unity/minpoly.lean b/src/ring_theory/roots_of_unity/minpoly.lean
@@ -10,6 +10,9 @@ import field_theory.minpoly.is_integrally_closed
 /-!
 # Minimal polynomial of roots of unity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We gather several results about minimal polynomial of root of unity.
 
 ## Main results
diff --git a/src/topology/category/UniformSpace.lean b/src/topology/category/UniformSpace.lean
@@ -12,6 +12,9 @@ import topology.uniform_space.completion
 /-!
 # The category of uniform spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the category of uniform spaces, show that the complete separated uniform spaces
 form a reflective subcategory, and hence possess all limits that uniform spaces do.
 
diff --git a/src/topology/continuous_function/zero_at_infty.lean b/src/topology/continuous_function/zero_at_infty.lean
@@ -9,6 +9,9 @@ import topology.continuous_function.cocompact_map
 /-!
 # Continuous functions vanishing at infinity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The type of continuous functions vanishing at infinity. When the domain is compact
 `C(α, β) ≃ C₀(α, β)` via the identity map. When the codomain is a metric space, every continuous
 map which vanishes at infinity is a bounded continuous function. When the domain is a locally
diff --git a/src/topology/sheaves/operations.lean b/src/topology/sheaves/operations.lean
@@ -12,6 +12,9 @@ import topology.sheaves.stalks
 
 # Operations on sheaves
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definition
 
 - `submonoid_presheaf` : A subpresheaf with a submonoid structure on each of the components.
