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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.direct_sum.algebra` * `algebra.direct_sum.ring` * `algebra.homology.opposite` * `algebra.homology.quasi_iso` * `algebraic_topology.fundamental_groupoid.basic` * `analysis.box_integral.partition.subbox_induction` * `analysis.complex.circle` * `analysis.normed_space.is_R_or_C` * `analysis.normed_space.operator_norm` * `analysis.special_functions.trigonometric.angle` * `analysis.special_functions.trigonometric.basic` * `analysis.special_functions.trigonometric.inverse` * `category_theory.limits.constructions.over.products` * `category_theory.preadditive.endo_functor` * `combinatorics.simple_graph.ends.properties` * `combinatorics.simple_graph.finsubgraph` * `linear_algebra.multilinear.finite_dimensional` * `ring_theory.free_comm_ring` * `ring_theory.polynomial.quotient` * `ring_theory.tensor_product` * `topology.algebra.module.finite_dimension` * `topology.metric_space.partition_of_unity`
leanprover-community · May 18, 2023 · 50251fd · 50251fd
1 parent c720ca1
commit 50251fd
Show file tree

Hide file tree

Showing 22 changed files with 66 additions and 0 deletions.
diff --git a/src/algebra/direct_sum/algebra.lean b/src/algebra/direct_sum/algebra.lean
@@ -9,6 +9,9 @@ import algebra.direct_sum.ring
 
 /-! # Additively-graded algebra structures on `⨁ i, A i`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides `R`-algebra structures on external direct sums of `R`-modules.
 
 Recall that if `A i` are a family of `add_comm_monoid`s indexed by an `add_monoid`, then an instance

diff --git a/src/algebra/direct_sum/ring.lean b/src/algebra/direct_sum/ring.lean
@@ -9,6 +9,9 @@ import algebra.direct_sum.basic
 /-!
 # Additively-graded multiplicative structures on `⨁ i, A i`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module provides a set of heterogeneous typeclasses for defining a multiplicative structure
 over `⨁ i, A i` such that `(*) : A i → A j → A (i + j)`; that is to say, `A` forms an
 additively-graded ring. The typeclasses are:

diff --git a/src/algebra/homology/opposite.lean b/src/algebra/homology/opposite.lean
@@ -10,6 +10,9 @@ import algebra.homology.additive
 
 /-!
 # Opposite categories of complexes
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Given a preadditive category `V`, the opposite of its category of chain complexes is equivalent to
 the category of cochain complexes of objects in `Vᵒᵖ`. We define this equivalence, and another
 analagous equivalence (for a general category of homological complexes with a general

diff --git a/src/algebra/homology/quasi_iso.lean b/src/algebra/homology/quasi_iso.lean
@@ -9,6 +9,9 @@ import category_theory.abelian.homology
 /-!
 # Quasi-isomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A chain map is a quasi-isomorphism if it induces isomorphisms on homology.
 
 ## Future work

diff --git a/src/algebraic_topology/fundamental_groupoid/basic.lean b/src/algebraic_topology/fundamental_groupoid/basic.lean
@@ -11,6 +11,9 @@ import topology.homotopy.path
 /-!
 # Fundamental groupoid of a space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a topological space `X`, we can define the fundamental groupoid of `X` to be the category with
 objects being points of `X`, and morphisms `x ⟶ y` being paths from `x` to `y`, quotiented by
 homotopy equivalence. With this, the fundamental group of `X` based at `x` is just the automorphism

diff --git a/src/analysis/box_integral/partition/subbox_induction.lean b/src/analysis/box_integral/partition/subbox_induction.lean
@@ -9,6 +9,9 @@ import analysis.box_integral.partition.tagged
 /-!
 # Induction on subboxes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove (see
 `box_integral.tagged_partition.exists_is_Henstock_is_subordinate_homothetic`) that for every box `I`
 in `ℝⁿ` and a function `r : ℝⁿ → ℝ` positive on `I` there exists a tagged partition `π` of `I` such

diff --git a/src/analysis/complex/circle.lean b/src/analysis/complex/circle.lean
@@ -10,6 +10,9 @@ import analysis.normed.field.unit_ball
 /-!
 # The circle
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `circle` to be the metric sphere (`metric.sphere`) in `ℂ` centred at `0` of
 radius `1`.  We equip it with the following structure:
 

diff --git a/src/analysis/normed_space/is_R_or_C.lean b/src/analysis/normed_space/is_R_or_C.lean
@@ -10,6 +10,9 @@ import analysis.normed_space.pointwise
 /-!
 # Normed spaces over R or C
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file is about results on normed spaces over the fields `ℝ` and `ℂ`.
 
 ## Main definitions

diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean
@@ -12,6 +12,9 @@ import topology.algebra.module.strong_topology
 /-!
 # Operator norm on the space of continuous linear maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Define the operator norm on the space of continuous (semi)linear maps between normed spaces, and
 prove its basic properties. In particular, show that this space is itself a normed space.
 

diff --git a/src/analysis/special_functions/trigonometric/angle.lean b/src/analysis/special_functions/trigonometric/angle.lean
@@ -11,6 +11,9 @@ import topology.instances.sign
 /-!
 # The type of angles
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `real.angle` to be the quotient group `ℝ/2πℤ` and prove a few simple lemmas
 about trigonometric functions and angles.
 -/

diff --git a/src/analysis/special_functions/trigonometric/basic.lean b/src/analysis/special_functions/trigonometric/basic.lean
@@ -8,6 +8,9 @@ import analysis.special_functions.exp
 /-!
 # Trigonometric functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 This file contains the definition of `π`.

diff --git a/src/analysis/special_functions/trigonometric/inverse.lean b/src/analysis/special_functions/trigonometric/inverse.lean
@@ -10,6 +10,9 @@ import topology.algebra.order.proj_Icc
 /-!
 # Inverse trigonometric functions.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 See also `analysis.special_functions.trigonometric.arctan` for the inverse tan function.
 (This is delayed as it is easier to set up after developing complex trigonometric functions.)
 

diff --git a/src/category_theory/limits/constructions/over/products.lean b/src/category_theory/limits/constructions/over/products.lean
@@ -11,6 +11,9 @@ import category_theory.limits.shapes.finite_products
 /-!
 # Products in the over category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Shows that products in the over category can be derived from wide pullbacks in the base category.
 The main result is `over_product_of_wide_pullback`, which says that if `C` has `J`-indexed wide
 pullbacks, then `over B` has `J`-indexed products.

diff --git a/src/category_theory/preadditive/endo_functor.lean b/src/category_theory/preadditive/endo_functor.lean
@@ -11,6 +11,9 @@ import category_theory.preadditive.additive_functor
 /-!
 # Preadditive structure on algebras over a monad
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `C` is a preadditive categories and `F` is an additive endofunctor on `C` then `algebra F` is
 also preadditive. Dually, the category `coalgebra F` is also preadditive.
 -/

diff --git a/src/combinatorics/simple_graph/ends/properties.lean b/src/combinatorics/simple_graph/ends/properties.lean
@@ -7,6 +7,9 @@ import combinatorics.simple_graph.ends.defs
 /-!
 # Properties of the ends of graphs
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file is meant to contain results about the ends of (locally finite connected) graphs.
 
 -/

diff --git a/src/combinatorics/simple_graph/finsubgraph.lean b/src/combinatorics/simple_graph/finsubgraph.lean
@@ -9,6 +9,9 @@ import combinatorics.simple_graph.subgraph
 /-!
 # Homomorphisms from finite subgraphs
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the type of finite subgraphs of a `simple_graph` and proves a compactness result
 for homomorphisms to a finite codomain.
 

diff --git a/src/linear_algebra/multilinear/finite_dimensional.lean b/src/linear_algebra/multilinear/finite_dimensional.lean
@@ -8,6 +8,9 @@ import linear_algebra.free_module.finite.matrix
 
 /-! # Multilinear maps over finite dimensional spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The main results are that multilinear maps over finitely-generated, free modules are
 finitely-generated and free.
 

diff --git a/src/ring_theory/free_comm_ring.lean b/src/ring_theory/free_comm_ring.lean
@@ -11,6 +11,9 @@ import ring_theory.free_ring
 /-!
 # Free commutative rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The theory of the free commutative ring generated by a type `α`.
 It is isomorphic to the polynomial ring over ℤ with variables
 in `α`

diff --git a/src/ring_theory/polynomial/quotient.lean b/src/ring_theory/polynomial/quotient.lean
@@ -10,6 +10,9 @@ import ring_theory.ideal.quotient_operations
 
 /-!
 # Quotients of polynomial rings
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open_locale polynomial

diff --git a/src/ring_theory/tensor_product.lean b/src/ring_theory/tensor_product.lean
@@ -11,6 +11,9 @@ import linear_algebra.direct_sum.finsupp
 /-!
 # The tensor product of R-algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `R` be a (semi)ring and `A` an `R`-algebra.
 In this file we:
 

diff --git a/src/topology/algebra/module/finite_dimension.lean b/src/topology/algebra/module/finite_dimension.lean
@@ -11,6 +11,9 @@ import topology.algebra.module.determinant
 /-!
 # Finite dimensional topological vector spaces over complete fields
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `𝕜` be a complete nontrivially normed field, and `E` a topological vector space (TVS) over
 `𝕜` (i.e we have `[add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E]`
 and `[has_continuous_smul 𝕜 E]`).

diff --git a/src/topology/metric_space/partition_of_unity.lean b/src/topology/metric_space/partition_of_unity.lean
@@ -9,6 +9,9 @@ import analysis.convex.partition_of_unity
 /-!
 # Lemmas about (e)metric spaces that need partition of unity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The main lemma in this file (see `metric.exists_continuous_real_forall_closed_ball_subset`) says the
 following. Let `X` be a metric space. Let `K : ι → set X` be a locally finite family of closed sets,
 let `U : ι → set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there exists a