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

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.projective` * `algebra.monoid_algebra.to_direct_sum` * `analysis.convex.strict_convex_space` * `analysis.convex.uniform` * `analysis.normed_space.banach` * `analysis.normed_space.bounded_linear_maps` * `analysis.normed_space.complemented` * `analysis.normed_space.finite_dimension` * `analysis.normed_space.mazur_ulam` * `analysis.special_functions.log.base` * `analysis.special_functions.log.monotone` * `analysis.special_functions.pow.real` * `combinatorics.additive.salem_spencer` * `data.is_R_or_C.lemmas` * `linear_algebra.adic_completion` * `linear_algebra.cross_product` * `measure_theory.measure.doubling` * `ring_theory.graded_algebra.basic` * `ring_theory.mv_polynomial.homogeneous` * `ring_theory.valuation.extend_to_localization` * `topology.algebra.module.star`
leanprover-community · May 21, 2023 · 1b0a28e · 1b0a28e
1 parent 33c67ae
commit 1b0a28e
Show file tree

Hide file tree

Showing 21 changed files with 64 additions and 1 deletion.
diff --git a/src/algebra/category/Module/projective.lean b/src/algebra/category/Module/projective.lean
@@ -10,6 +10,9 @@ import linear_algebra.finsupp_vector_space
 
 /-!
 # The category of `R`-modules has enough projectives.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 universes v u

diff --git a/src/algebra/monoid_algebra/to_direct_sum.lean b/src/algebra/monoid_algebra/to_direct_sum.lean
@@ -10,6 +10,9 @@ import data.finsupp.to_dfinsupp
 /-!
 # Conversion between `add_monoid_algebra` and homogenous `direct_sum`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module provides conversions between `add_monoid_algebra` and `direct_sum`.
 The latter is essentially a dependent version of the former.
 

diff --git a/src/analysis/convex/strict_convex_space.lean b/src/analysis/convex/strict_convex_space.lean
@@ -13,6 +13,9 @@ import analysis.normed_space.affine_isometry
 /-!
 # Strictly convex spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines strictly convex spaces. A normed space is strictly convex if all closed balls are
 strictly convex. This does **not** mean that the norm is strictly convex (in fact, it never is).
 

diff --git a/src/analysis/convex/uniform.lean b/src/analysis/convex/uniform.lean
@@ -8,6 +8,9 @@ import analysis.convex.strict_convex_space
 /-!
 # Uniformly convex spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines uniformly convex spaces, which are real normed vector spaces in which for all
 strictly positive `ε`, there exists some strictly positive `δ` such that `ε ≤ ‖x - y‖` implies
 `‖x + y‖ ≤ 2 - δ` for all `x` and `y` of norm at most than `1`. This means that the triangle

diff --git a/src/analysis/normed_space/banach.lean b/src/analysis/normed_space/banach.lean
@@ -10,6 +10,9 @@ import analysis.normed_space.affine_isometry
 /-!
 # Banach open mapping theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains the Banach open mapping theorem, i.e., the fact that a bijective
 bounded linear map between Banach spaces has a bounded inverse.
 -/

diff --git a/src/analysis/normed_space/bounded_linear_maps.lean b/src/analysis/normed_space/bounded_linear_maps.lean
@@ -10,6 +10,9 @@ import analysis.asymptotics.asymptotics
 /-!
 # Bounded linear maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines a class stating that a map between normed vector spaces is (bi)linear and
 continuous.
 Instead of asking for continuity, the definition takes the equivalent condition (because the space

diff --git a/src/analysis/normed_space/complemented.lean b/src/analysis/normed_space/complemented.lean
@@ -9,6 +9,9 @@ import analysis.normed_space.finite_dimension
 /-!
 # Complemented subspaces of normed vector spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A submodule `p` of a topological module `E` over `R` is called *complemented* if there exists
 a continuous linear projection `f : E →ₗ[R] p`, `∀ x : p, f x = x`. We prove that for
 a closed subspace of a normed space this condition is equivalent to existence of a closed

diff --git a/src/analysis/normed_space/finite_dimension.lean b/src/analysis/normed_space/finite_dimension.lean
@@ -15,6 +15,9 @@ import topology.instances.matrix
 /-!
 # Finite dimensional normed spaces over complete fields
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Over a complete nontrivially normed field, in finite dimension, all norms are equivalent and all
 linear maps are continuous. Moreover, a finite-dimensional subspace is always complete and closed.
 

diff --git a/src/analysis/normed_space/mazur_ulam.lean b/src/analysis/normed_space/mazur_ulam.lean
@@ -9,6 +9,9 @@ import analysis.normed_space.affine_isometry
 /-!
 # Mazur-Ulam Theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Mazur-Ulam theorem states that an isometric bijection between two normed affine spaces over `ℝ` is
 affine. We formalize it in three definitions:
 

diff --git a/src/analysis/special_functions/log/base.lean b/src/analysis/special_functions/log/base.lean
@@ -9,6 +9,9 @@ import data.int.log
 /-!
 # Real logarithm base `b`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `real.logb` to be the logarithm of a real number in a given base `b`. We
 define this as the division of the natural logarithms of the argument and the base, so that we have
 a globally defined function with `logb b 0 = 0`, `logb b (-x) = logb b x` `logb 0 x = 0` and

diff --git a/src/analysis/special_functions/log/monotone.lean b/src/analysis/special_functions/log/monotone.lean
@@ -8,6 +8,9 @@ import analysis.special_functions.pow.real
 /-!
 # Logarithm Tonality
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we describe the tonality of the logarithm function when multiplied by functions of the
 form `x ^ a`.
 

diff --git a/src/analysis/special_functions/pow/real.lean b/src/analysis/special_functions/pow/real.lean
@@ -8,6 +8,9 @@ import analysis.special_functions.pow.complex
 
 /-! # Power function on `ℝ`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the power functions `x ^ y`, where `x` and `y` are real numbers.
 -/
 

diff --git a/src/combinatorics/additive/salem_spencer.lean b/src/combinatorics/additive/salem_spencer.lean
@@ -10,6 +10,9 @@ import analysis.convex.strict_convex_space
 /-!
 # Salem-Spencer sets and Roth numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines Salem-Spencer sets and the Roth number of a set.
 
 A Salem-Spencer set is a set without arithmetic progressions of length `3`. Equivalently, the

diff --git a/src/data/is_R_or_C/lemmas.lean b/src/data/is_R_or_C/lemmas.lean
@@ -7,7 +7,10 @@ import analysis.normed_space.finite_dimension
 import field_theory.tower
 import data.is_R_or_C.basic
 
-/-! # Further lemmas about `is_R_or_C` -/
+/-! # Further lemmas about `is_R_or_C` 
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.-/
 
 variables {K E : Type*} [is_R_or_C K]
 

diff --git a/src/linear_algebra/adic_completion.lean b/src/linear_algebra/adic_completion.lean
@@ -11,6 +11,9 @@ import ring_theory.jacobson_ideal
 /-!
 # Completion of a module with respect to an ideal.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the notions of Hausdorff, precomplete, and complete for an `R`-module `M`
 with respect to an ideal `I`:
 

diff --git a/src/linear_algebra/cross_product.lean b/src/linear_algebra/cross_product.lean
@@ -12,6 +12,9 @@ import algebra.lie.basic
 /-!
 # Cross products
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module defines the cross product of vectors in $R^3$ for $R$ a commutative ring,
 as a bilinear map.
 

diff --git a/src/measure_theory/measure/doubling.lean b/src/measure_theory/measure/doubling.lean
@@ -9,6 +9,9 @@ import measure_theory.measure.measure_space_def
 /-!
 # Uniformly locally doubling measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A uniformly locally doubling measure `μ` on a metric space is a measure for which there exists a
 constant `C` such that for all sufficiently small radii `ε`, and for any centre, the measure of a
 ball of radius `2 * ε` is bounded by `C` times the measure of the concentric ball of radius `ε`.

diff --git a/src/ring_theory/graded_algebra/basic.lean b/src/ring_theory/graded_algebra/basic.lean
@@ -11,6 +11,9 @@ import algebra.direct_sum.ring
 /-!
 # Internally-graded rings and algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the typeclass `graded_algebra 𝒜`, for working with an algebra `A` that is
 internally graded by a collection of submodules `𝒜 : ι → submodule R A`.
 See the docstring of that typeclass for more information.

diff --git a/src/ring_theory/mv_polynomial/homogeneous.lean b/src/ring_theory/mv_polynomial/homogeneous.lean
@@ -10,6 +10,9 @@ import data.mv_polynomial.variables
 /-!
 # Homogeneous polynomials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A multivariate polynomial `φ` is homogeneous of degree `n`
 if all monomials occuring in `φ` have degree `n`.
 

diff --git a/src/ring_theory/valuation/extend_to_localization.lean b/src/ring_theory/valuation/extend_to_localization.lean
@@ -10,6 +10,9 @@ import ring_theory.valuation.basic
 
 # Extending valuations to a localization
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show that, given a valuation `v` taking values in a linearly ordered commutative *group*
 with zero `Γ`, and a submonoid `S` of `v.supp.prime_compl`, the valuation `v` can be naturally
 extended to the localization `S⁻¹A`.

diff --git a/src/topology/algebra/module/star.lean b/src/topology/algebra/module/star.lean
@@ -9,6 +9,9 @@ import topology.algebra.star
 
 /-!
 # The star operation, bundled as a continuous star-linear equiv
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 /-- If `A` is a topological module over a commutative `R` with compatible actions,