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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Module.adjunctions` * `analysis.calculus.darboux` * `analysis.calculus.deriv.inv` * `analysis.calculus.diff_cont_on_cl` * `analysis.calculus.dslope` * `analysis.inner_product_space.gram_schmidt_ortho` * `category_theory.abelian.ext` * `category_theory.abelian.left_derived` * `category_theory.bicategory.single_obj` * `data.real.golden_ratio` * `measure_theory.category.Meas` * `measure_theory.decomposition.jordan` * `measure_theory.decomposition.signed_hahn` * `measure_theory.group.action` * `measure_theory.group.measure` * `number_theory.arithmetic_function` * `number_theory.l_series` * `number_theory.von_mangoldt` * `topology.algebra.continuous_monoid_hom` * `topology.instances.discrete` * `topology.sheaves.stalks` * `topology.tietze_extension`
leanprover-community · May 31, 2023 · 61b5e27 · 61b5e27
1 parent 12a85fa
commit 61b5e27
Show file tree

Hide file tree

Showing 22 changed files with 66 additions and 0 deletions.
diff --git a/src/algebra/category/Module/adjunctions.lean b/src/algebra/category/Module/adjunctions.lean
@@ -10,6 +10,9 @@ import linear_algebra.direct_sum.finsupp
 import category_theory.linear.linear_functor
 
 /-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The functor of forming finitely supported functions on a type with values in a `[ring R]`
 is the left adjoint of
 the forgetful functor from `R`-modules to types.

diff --git a/src/analysis/calculus/darboux.lean b/src/analysis/calculus/darboux.lean
@@ -8,6 +8,9 @@ import analysis.calculus.local_extr
 /-!
 # Darboux's theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that the derivative of a differentiable function on an interval takes all
 intermediate values. The proof is based on the
 [Wikipedia](https://en.wikipedia.org/wiki/Darboux%27s_theorem_(analysis)) page about this theorem.

diff --git a/src/analysis/calculus/deriv/inv.lean b/src/analysis/calculus/deriv/inv.lean
@@ -9,6 +9,9 @@ import analysis.calculus.deriv.comp
 /-!
 # Derivatives of `x ↦ x⁻¹` and `f x / g x`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove `(x⁻¹)' = -1 / x ^ 2`, `((f x)⁻¹)' = -f' x / (f x) ^ 2`, and
 `(f x / g x)' = (f' x * g x - f x * g' x) / (g x) ^ 2` for different notions of derivative.
 

diff --git a/src/analysis/calculus/diff_cont_on_cl.lean b/src/analysis/calculus/diff_cont_on_cl.lean
@@ -8,6 +8,9 @@ import analysis.calculus.deriv.inv
 /-!
 # Functions differentiable on a domain and continuous on its closure
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Many theorems in complex analysis assume that a function is complex differentiable on a domain and
 is continuous on its closure. In this file we define a predicate `diff_cont_on_cl` that expresses
 this property and prove basic facts about this predicate.

diff --git a/src/analysis/calculus/dslope.lean b/src/analysis/calculus/dslope.lean
@@ -9,6 +9,9 @@ import analysis.calculus.deriv.inv
 /-!
 # Slope of a differentiable function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a function `f : 𝕜 → E` from a nontrivially normed field to a normed space over this field,
 `dslope f a b` is defined as `slope f a b = (b - a)⁻¹ • (f b - f a)` for `a ≠ b` and as `deriv f a`
 for `a = b`.

diff --git a/src/analysis/inner_product_space/gram_schmidt_ortho.lean b/src/analysis/inner_product_space/gram_schmidt_ortho.lean
@@ -10,6 +10,9 @@ import linear_algebra.matrix.block
 /-!
 # Gram-Schmidt Orthogonalization and Orthonormalization
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we introduce Gram-Schmidt Orthogonalization and Orthonormalization.
 
 The Gram-Schmidt process takes a set of vectors as input

diff --git a/src/category_theory/abelian/ext.lean b/src/category_theory/abelian/ext.lean
@@ -12,6 +12,9 @@ import category_theory.abelian.projective
 /-!
 # Ext
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define `Ext R C n : Cᵒᵖ ⥤ C ⥤ Module R` for any `R`-linear abelian category `C`
 by (left) deriving in the first argument of the bifunctor `(X, Y) ↦ Module.of R (unop X ⟶ Y)`.
 

diff --git a/src/category_theory/abelian/left_derived.lean b/src/category_theory/abelian/left_derived.lean
@@ -12,6 +12,9 @@ import category_theory.limits.constructions.epi_mono
 /-!
 # Zeroth left derived functors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `F : C ⥤ D` is an additive right exact functor between abelian categories, where `C` has enough
 projectives, we provide the natural isomorphism `F.left_derived 0 ≅ F`.
 

diff --git a/src/category_theory/bicategory/single_obj.lean b/src/category_theory/bicategory/single_obj.lean
@@ -9,6 +9,9 @@ import category_theory.monoidal.functor
 /-!
 # Promoting a monoidal category to a single object bicategory.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A monoidal category can be thought of as a bicategory with a single object.
 
 The objects of the monoidal category become the 1-morphisms,

diff --git a/src/data/real/golden_ratio.lean b/src/data/real/golden_ratio.lean
@@ -13,6 +13,9 @@ import algebra.linear_recurrence
 /-!
 # The golden ratio and its conjugate
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the golden ratio `φ := (1 + √5)/2` and its conjugate
 `ψ := (1 - √5)/2`, which are the two real roots of `X² - X - 1`.
 

diff --git a/src/measure_theory/category/Meas.lean b/src/measure_theory/category/Meas.lean
@@ -11,6 +11,9 @@ import topology.category.Top.basic
 /-!
 # The category of measurable spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Measurable spaces and measurable functions form a (concrete) category `Meas`.
 
 ## Main definitions

diff --git a/src/measure_theory/decomposition/jordan.lean b/src/measure_theory/decomposition/jordan.lean
@@ -9,6 +9,9 @@ import measure_theory.measure.mutually_singular
 /-!
 # Jordan decomposition
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the existence and uniqueness of the Jordan decomposition for signed measures.
 The Jordan decomposition theorem states that, given a signed measure `s`, there exists a
 unique pair of mutually singular measures `μ` and `ν`, such that `s = μ - ν`.

diff --git a/src/measure_theory/decomposition/signed_hahn.lean b/src/measure_theory/decomposition/signed_hahn.lean
@@ -9,6 +9,9 @@ import order.symm_diff
 /-!
 # Hahn decomposition
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the Hahn decomposition theorem (signed version). The Hahn decomposition theorem
 states that, given a signed measure `s`, there exist complementary, measurable sets `i` and `j`,
 such that `i` is positive and `j` is negative with respect to `s`; that is, `s` restricted on `i`

diff --git a/src/measure_theory/group/action.lean b/src/measure_theory/group/action.lean
@@ -11,6 +11,9 @@ import dynamics.minimal
 /-!
 # Measures invariant under group actions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A measure `μ : measure α` is said to be *invariant* under an action of a group `G` if scalar
 multiplication by `c : G` is a measure preserving map for all `c`. In this file we define a
 typeclass for measures invariant under action of an (additive or multiplicative) group and prove

diff --git a/src/measure_theory/group/measure.lean b/src/measure_theory/group/measure.lean
@@ -14,6 +14,9 @@ import topology.continuous_function.cocompact_map
 /-!
 # Measures on Groups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We develop some properties of measures on (topological) groups
 
 * We define properties on measures: measures that are left or right invariant w.r.t. multiplication.

diff --git a/src/number_theory/arithmetic_function.lean b/src/number_theory/arithmetic_function.lean
@@ -14,6 +14,9 @@ import data.nat.factorization.basic
 /-!
 # Arithmetic Functions and Dirichlet Convolution
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines arithmetic functions, which are functions from `ℕ` to a specified type that map 0
 to 0. In the literature, they are often instead defined as functions from `ℕ+`. These arithmetic
 functions are endowed with a multiplication, given by Dirichlet convolution, and pointwise addition,

diff --git a/src/number_theory/l_series.lean b/src/number_theory/l_series.lean
@@ -11,6 +11,9 @@ import topology.algebra.infinite_sum.basic
 /-!
 # L-series
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given an arithmetic function, we define the corresponding L-series.
 
 ## Main Definitions

diff --git a/src/number_theory/von_mangoldt.lean b/src/number_theory/von_mangoldt.lean
@@ -11,6 +11,9 @@ import analysis.special_functions.log.basic
 /-!
 # The von Mangoldt Function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the von Mangoldt function: the function on natural numbers that returns
 `log p` if the input can be expressed as `p^k` for a prime `p`.
 

diff --git a/src/topology/algebra/continuous_monoid_hom.lean b/src/topology/algebra/continuous_monoid_hom.lean
@@ -10,6 +10,9 @@ import topology.continuous_function.algebra
 
 # Continuous Monoid Homs
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the space of continuous homomorphisms between two topological groups.
 
 ## Main definitions

diff --git a/src/topology/instances/discrete.lean b/src/topology/instances/discrete.lean
@@ -11,6 +11,9 @@ import topology.metric_space.metrizable_uniformity
 /-!
 # Instances related to the discrete topology
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove that the discrete topology is
 * first-countable,
 * second-countable for an encodable type,

diff --git a/src/topology/sheaves/stalks.lean b/src/topology/sheaves/stalks.lean
@@ -17,6 +17,9 @@ import category_theory.sites.pushforward
 /-!
 # Stalks
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For a presheaf `F` on a topological space `X`, valued in some category `C`, the *stalk* of `F`
 at the point `x : X` is defined as the colimit of the composition of the inclusion of categories
 `(nhds x)ᵒᵖ ⥤ (opens X)ᵒᵖ` and the functor `F : (opens X)ᵒᵖ ⥤ C`.

diff --git a/src/topology/tietze_extension.lean b/src/topology/tietze_extension.lean
@@ -11,6 +11,9 @@ import topology.urysohns_bounded
 /-!
 # Tietze extension theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove a few version of the Tietze extension theorem. The theorem says that a
 continuous function `s → ℝ` defined on a closed set in a normal topological space `Y` can be
 extended to a continuous function on the whole space. Moreover, if all values of the original