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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Group.abelian` * `algebra.category.Group.colimits` * `algebra.category.Group.images` * `algebra.category.Module.abelian` * `algebra.category.Module.biproducts` * `algebra.category.Module.images` * `algebra.category.Ring.constructions` * `algebra.category.Ring.filtered_colimits` * `algebra.category.Ring.limits` * `algebra.module.graded_module` * `algebra.module.torsion` * `algebraic_geometry.presheafed_space.has_colimits` * `algebraic_geometry.prime_spectrum.maximal` * `algebraic_geometry.prime_spectrum.noetherian` * `algebraic_geometry.sheafed_space` * `analysis.box_integral.partition.filter` * `analysis.calculus.conformal.inner_product` * `analysis.calculus.conformal.normed_space` * `analysis.calculus.fderiv.bilinear` * `analysis.calculus.fderiv.mul` * `analysis.complex.arg` * `analysis.complex.conformal` * `analysis.complex.unit_disc.basic` * `analysis.convex.krein_milman` * `analysis.convex.specific_functions.basic` * `analysis.inner_product_space.basic` * `analysis.inner_product_space.conformal_linear_map` * `analysis.inner_product_space.dual` * `analysis.inner_product_space.orthogonal` * `analysis.inner_product_space.projection` * `analysis.inner_product_space.symmetric` * `analysis.locally_convex.abs_convex` * `analysis.locally_convex.weak_dual` * `analysis.mean_inequalities` * `analysis.mean_inequalities_pow` * `analysis.normed_space.dual` * `analysis.normed_space.hahn_banach.separation` * `analysis.normed_space.pi_Lp` * `analysis.normed_space.star.multiplier` * `analysis.normed_space.weak_dual` * `analysis.p_series` * `analysis.special_functions.pow.asymptotics` * `analysis.special_functions.pow.continuity` * `category_theory.abelian.injective` * `category_theory.abelian.injective_resolution` * `category_theory.abelian.projective` * `category_theory.abelian.right_derived` * `category_theory.preadditive.yoneda.limits` * `data.nat.squarefree` * `data.zmod.quotient` * `field_theory.ratfunc` * `geometry.euclidean.angle.unoriented.affine` * `geometry.euclidean.angle.unoriented.basic` * `geometry.euclidean.angle.unoriented.conformal` * `geometry.euclidean.basic` * `geometry.euclidean.inversion` * `geometry.manifold.conformal_groupoid` * `group_theory.exponent` * `group_theory.p_group` * `group_theory.specific_groups.cyclic` * `group_theory.specific_groups.dihedral` * `group_theory.torsion` * `linear_algebra.free_module.ideal_quotient` * `linear_algebra.matrix.bilinear_form` * `linear_algebra.matrix.sesquilinear_form` * `measure_theory.function.egorov` * `measure_theory.function.special_functions.inner` * `measure_theory.function.strongly_measurable.inner` * `measure_theory.integral.mean_inequalities` * `model_theory.graph` * `model_theory.satisfiability` * `model_theory.types` * `model_theory.ultraproducts` * `number_theory.bernoulli` * `number_theory.padics.hensel` * `number_theory.padics.padic_integers` * `order.category.FinPartOrd` * `probability.probability_mass_function.constructions` * `ring_theory.adjoin.field` * `ring_theory.algebraic_independent` * `ring_theory.integral_domain` * `ring_theory.is_tensor_product` * `ring_theory.polynomial.dickson` * `topology.continuous_function.compact` * `topology.instances.complex` * `topology.metric_space.holder` * `topology.sheaves.functors` * `topology.sheaves.sheaf_condition.equalizer_products` * `topology.sheaves.sheaf_condition.pairwise_intersections`
leanprover-community · May 27, 2023 · 0b7c740 · 0b7c740
1 parent c4015ac
commit 0b7c740
Show file tree

Hide file tree

Showing 89 changed files with 267 additions and 0 deletions.
diff --git a/src/algebra/category/Group/abelian.lean b/src/algebra/category/Group/abelian.lean
@@ -11,6 +11,9 @@ import category_theory.abelian.basic
 
 /-!
 # The category of abelian groups is abelian
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open category_theory

diff --git a/src/algebra/category/Group/colimits.lean b/src/algebra/category/Group/colimits.lean
@@ -11,6 +11,9 @@ import category_theory.concrete_category.elementwise
 /-!
 # The category of additive commutative groups has all colimits.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file uses a "pre-automated" approach, just as for `Mon/colimits.lean`.
 It is a very uniform approach, that conceivably could be synthesised directly
 by a tactic that analyses the shape of `add_comm_group` and `monoid_hom`.

diff --git a/src/algebra/category/Group/images.lean b/src/algebra/category/Group/images.lean
@@ -9,6 +9,9 @@ import category_theory.limits.shapes.images
 /-!
 # The category of commutative additive groups has images.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Note that we don't need to register any of the constructions here as instances, because we get them
 from the fact that `AddCommGroup` is an abelian category.
 -/

diff --git a/src/algebra/category/Module/abelian.lean b/src/algebra/category/Module/abelian.lean
@@ -11,6 +11,9 @@ import category_theory.abelian.exact
 /-!
 # The category of left R-modules is abelian.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Additionally, two linear maps are exact in the categorical sense iff `range f = ker g`.
 -/
 

diff --git a/src/algebra/category/Module/biproducts.lean b/src/algebra/category/Module/biproducts.lean
@@ -10,6 +10,9 @@ import algebra.homology.short_exact.abelian
 
 /-!
 # The category of `R`-modules has finite biproducts
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open category_theory

diff --git a/src/algebra/category/Module/images.lean b/src/algebra/category/Module/images.lean
@@ -9,6 +9,9 @@ import category_theory.limits.shapes.images
 /-!
 # The category of R-modules has images.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Note that we don't need to register any of the constructions here as instances, because we get them
 from the fact that `Module R` is an abelian category.
 -/

diff --git a/src/algebra/category/Ring/constructions.lean b/src/algebra/category/Ring/constructions.lean
@@ -13,6 +13,9 @@ import ring_theory.subring.basic
 /-!
 # Constructions of (co)limits in CommRing
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we provide the explicit (co)cones for various (co)limits in `CommRing`, including
 * tensor product is the pushout
 * `Z` is the initial object

diff --git a/src/algebra/category/Ring/filtered_colimits.lean b/src/algebra/category/Ring/filtered_colimits.lean
@@ -9,6 +9,9 @@ import algebra.category.Group.filtered_colimits
 /-!
 # The forgetful functor from (commutative) (semi-) rings preserves filtered colimits.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend
 to preserve _filtered_ colimits.
 

diff --git a/src/algebra/category/Ring/limits.lean b/src/algebra/category/Ring/limits.lean
@@ -11,6 +11,9 @@ import ring_theory.subring.basic
 /-!
 # The category of (commutative) rings has all limits
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Further, these limits are preserved by the forgetful functor --- that is,
 the underlying types are just the limits in the category of types.
 -/

diff --git a/src/algebra/module/graded_module.lean b/src/algebra/module/graded_module.lean
@@ -12,6 +12,9 @@ import algebra.module.big_operators
 /-!
 # Graded Module
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given an `R`-algebra `A` graded by `𝓐`, a graded `A`-module `M` is expressed as
 `direct_sum.decomposition 𝓜` and `set_like.has_graded_smul 𝓐 𝓜`.
 Then `⨁ i, 𝓜 i` is an `A`-module and is isomorphic to `M`.

diff --git a/src/algebra/module/torsion.lean b/src/algebra/module/torsion.lean
@@ -13,6 +13,9 @@ import ring_theory.finiteness
 /-!
 # Torsion submodules
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 * `torsion_of R M x` : the torsion ideal of `x`, containing all `a` such that `a • x = 0`.

diff --git a/src/algebraic_geometry/presheafed_space/has_colimits.lean b/src/algebraic_geometry/presheafed_space/has_colimits.lean
@@ -10,6 +10,9 @@ import topology.sheaves.limits
 /-!
 # `PresheafedSpace C` has colimits.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `C` has limits, then the category `PresheafedSpace C` has colimits,
 and the forgetful functor to `Top` preserves these colimits.
 

diff --git a/src/algebraic_geometry/prime_spectrum/maximal.lean b/src/algebraic_geometry/prime_spectrum/maximal.lean
@@ -10,6 +10,9 @@ import ring_theory.localization.as_subring
 /-!
 # Maximal spectrum of a commutative ring
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The maximal spectrum of a commutative ring is the type of all maximal ideals.
 It is naturally a subset of the prime spectrum endowed with the subspace topology.
 

diff --git a/src/algebraic_geometry/prime_spectrum/noetherian.lean b/src/algebraic_geometry/prime_spectrum/noetherian.lean
@@ -6,6 +6,9 @@ Authors: Filippo A. E. Nuccio, Andrew Yang
 import algebraic_geometry.prime_spectrum.basic
 import topology.noetherian_space
 /-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves additional properties of the prime spectrum a ring is Noetherian.
 -/
 

diff --git a/src/algebraic_geometry/sheafed_space.lean b/src/algebraic_geometry/sheafed_space.lean
@@ -9,6 +9,9 @@ import topology.sheaves.functors
 /-!
 # Sheafed spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Introduces the category of topological spaces equipped with a sheaf (taking values in an
 arbitrary target category `C`.)
 

diff --git a/src/analysis/box_integral/partition/filter.lean b/src/analysis/box_integral/partition/filter.lean
@@ -9,6 +9,9 @@ import analysis.box_integral.partition.split
 /-!
 # Filters used in box-based integrals
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 First we define a structure `box_integral.integration_params`. This structure will be used as an
 argument in the definition of `box_integral.integral` in order to use the same definition for a few
 well-known definitions of integrals based on partitions of a rectangular box into subboxes (Riemann

diff --git a/src/analysis/calculus/conformal/inner_product.lean b/src/analysis/calculus/conformal/inner_product.lean
@@ -9,6 +9,9 @@ import analysis.inner_product_space.conformal_linear_map
 /-!
 # Conformal maps between inner product spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A function between inner product spaces is which has a derivative at `x`
 is conformal at `x` iff the derivative preserves inner products up to a scalar multiple.
 -/

diff --git a/src/analysis/calculus/conformal/normed_space.lean b/src/analysis/calculus/conformal/normed_space.lean
@@ -12,6 +12,9 @@ import analysis.calculus.fderiv.restrict_scalars
 /-!
 # Conformal Maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A continuous linear map between real normed spaces `X` and `Y` is `conformal_at` some point `x`
 if it is real differentiable at that point and its differential `is_conformal_linear_map`.
 

diff --git a/src/analysis/calculus/fderiv/bilinear.lean b/src/analysis/calculus/fderiv/bilinear.lean
@@ -8,6 +8,9 @@ import analysis.calculus.fderiv.prod
 /-!
 # The derivative of bounded bilinear maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For detailed documentation of the Fréchet derivative,
 see the module docstring of `analysis/calculus/fderiv/basic.lean`.
 

diff --git a/src/analysis/calculus/fderiv/mul.lean b/src/analysis/calculus/fderiv/mul.lean
@@ -8,6 +8,9 @@ import analysis.calculus.fderiv.bilinear
 /-!
 # Multiplicative operations on derivatives
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For detailed documentation of the Fréchet derivative,
 see the module docstring of `analysis/calculus/fderiv/basic.lean`.
 

diff --git a/src/analysis/complex/arg.lean b/src/analysis/complex/arg.lean
@@ -10,6 +10,9 @@ import analysis.special_functions.complex.arg
 /-!
 # Rays in the complex numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file links the definition `same_ray ℝ x y` with the equality of arguments of complex numbers,
 the usual way this is considered.
 

diff --git a/src/analysis/complex/conformal.lean b/src/analysis/complex/conformal.lean
@@ -10,6 +10,9 @@ import analysis.normed_space.finite_dimension
 /-!
 # Conformal maps between complex vector spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove the sufficient and necessary conditions for a real-linear map between complex vector spaces
 to be conformal.
 

diff --git a/src/analysis/complex/unit_disc/basic.lean b/src/analysis/complex/unit_disc/basic.lean
@@ -9,6 +9,9 @@ import analysis.normed_space.ball_action
 /-!
 # Poincaré disc
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `complex.unit_disc` to be the unit disc in the complex plane. We also
 introduce some basic operations on this disc.
 -/

diff --git a/src/analysis/convex/krein_milman.lean b/src/analysis/convex/krein_milman.lean
@@ -9,6 +9,9 @@ import analysis.normed_space.hahn_banach.separation
 /-!
 # The Krein-Milman theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the Krein-Milman lemma and the Krein-Milman theorem.
 
 ## The lemma

diff --git a/src/analysis/convex/specific_functions/basic.lean b/src/analysis/convex/specific_functions/basic.lean
@@ -10,6 +10,9 @@ import tactic.linear_combination
 /-!
 # Collection of convex functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that the following functions are convex or strictly convex:
 
 * `strict_convex_on_exp` : The exponential function is strictly convex.

diff --git a/src/analysis/inner_product_space/basic.lean b/src/analysis/inner_product_space/basic.lean
@@ -13,6 +13,9 @@ import linear_algebra.bilinear_form
 /-!
 # Inner product space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines inner product spaces and proves the basic properties.  We do not formally
 define Hilbert spaces, but they can be obtained using the set of assumptions
 `[normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E]`.

diff --git a/src/analysis/inner_product_space/conformal_linear_map.lean b/src/analysis/inner_product_space/conformal_linear_map.lean
@@ -9,6 +9,9 @@ import analysis.inner_product_space.basic
 /-!
 # Conformal maps between inner product spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In an inner product space, a map is conformal iff it preserves inner products up to a scalar factor.
 -/
 

diff --git a/src/analysis/inner_product_space/dual.lean b/src/analysis/inner_product_space/dual.lean
@@ -10,6 +10,9 @@ import analysis.normed_space.star.basic
 /-!
 # The Fréchet-Riesz representation theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We consider an inner product space `E` over `𝕜`, which is either `ℝ` or `ℂ`. We define
 `to_dual_map`, a conjugate-linear isometric embedding of `E` into its dual, which maps an element
 `x` of the space to `λ y, ⟪x, y⟫`.

diff --git a/src/analysis/inner_product_space/orthogonal.lean b/src/analysis/inner_product_space/orthogonal.lean
@@ -9,6 +9,9 @@ import analysis.inner_product_space.basic
 /-!
 # Orthogonal complements of submodules
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, the `orthogonal` complement of a submodule `K` is defined, and basic API established.
 Some of the more subtle results about the orthogonal complement are delayed to
 `analysis.inner_product_space.projection`.

diff --git a/src/analysis/inner_product_space/projection.lean b/src/analysis/inner_product_space/projection.lean
@@ -13,6 +13,9 @@ import data.is_R_or_C.lemmas
 /-!
 # The orthogonal projection
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a nonempty complete subspace `K` of an inner product space `E`, this file constructs
 `orthogonal_projection K : E →L[𝕜] K`, the orthogonal projection of `E` onto `K`.  This map
 satisfies: for any point `u` in `E`, the point `v = orthogonal_projection K u` in `K` minimizes the

diff --git a/src/analysis/inner_product_space/symmetric.lean b/src/analysis/inner_product_space/symmetric.lean
@@ -10,6 +10,9 @@ import linear_algebra.sesquilinear_form
 /-!
 # Symmetric linear maps in an inner product space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines and proves basic theorems about symmetric **not necessarily bounded** operators
 on an inner product space, i.e linear maps `T : E → E` such that `∀ x y, ⟪T x, y⟫ = ⟪x, T y⟫`.
 

diff --git a/src/analysis/locally_convex/abs_convex.lean b/src/analysis/locally_convex/abs_convex.lean
@@ -10,6 +10,9 @@ import analysis.convex.gauge
 /-!
 # Absolutely convex sets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A set is called absolutely convex or disked if it is convex and balanced.
 The importance of absolutely convex sets comes from the fact that every locally convex
 topological vector space has a basis consisting of absolutely convex sets.

diff --git a/src/analysis/locally_convex/weak_dual.lean b/src/analysis/locally_convex/weak_dual.lean
@@ -10,6 +10,9 @@ import analysis.locally_convex.with_seminorms
 /-!
 # Weak Dual in Topological Vector Spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove that the weak topology induced by a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` is locally
 convex and we explicit give a neighborhood basis in terms of the family of seminorms `λ x, ‖B x y‖`
 for `y : F`.

diff --git a/src/analysis/mean_inequalities.lean b/src/analysis/mean_inequalities.lean
@@ -11,6 +11,9 @@ import data.real.conjugate_exponents
 /-!
 # Mean value inequalities
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove several inequalities for finite sums, including AM-GM inequality,
 Young's inequality, Hölder inequality, and Minkowski inequality. Versions for integrals of some of
 these inequalities are available in `measure_theory.mean_inequalities`.

diff --git a/src/analysis/mean_inequalities_pow.lean b/src/analysis/mean_inequalities_pow.lean
@@ -11,6 +11,9 @@ import tactic.positivity
 /-!
 # Mean value inequalities
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove several mean inequalities for finite sums. Versions for integrals of some of
 these inequalities are available in `measure_theory.mean_inequalities`.
 

diff --git a/src/analysis/normed_space/dual.lean b/src/analysis/normed_space/dual.lean
@@ -10,6 +10,9 @@ import analysis.locally_convex.polar
 /-!
 # The topological dual of a normed space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the topological dual `normed_space.dual` of a normed space, and the
 continuous linear map `normed_space.inclusion_in_double_dual` from a normed space into its double
 dual.

diff --git a/src/analysis/normed_space/hahn_banach/separation.lean b/src/analysis/normed_space/hahn_banach/separation.lean
@@ -11,6 +11,9 @@ import topology.algebra.module.locally_convex
 /-!
 # Separation Hahn-Banach theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the geometric Hahn-Banach theorem. For any two disjoint convex sets, there
 exists a continuous linear functional separating them, geometrically meaning that we can intercalate
 a plane between them.

diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
@@ -9,6 +9,9 @@ import linear_algebra.matrix.basis
 
 /-!
 # `L^p` distance on finite products of metric spaces
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Given finitely many metric spaces, one can put the max distance on their product, but there is also
 a whole family of natural distances, indexed by a parameter `p : ℝ≥0∞`, that also induce
 the product topology. We define them in this file. For `0 < p < ∞`, the distance on `Π i, α i`

diff --git a/src/analysis/normed_space/star/multiplier.lean b/src/analysis/normed_space/star/multiplier.lean
@@ -13,6 +13,9 @@ import analysis.normed_space.star.mul
 /-!
 # Multiplier Algebra of a C⋆-algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Define the multiplier algebra of a C⋆-algebra as the algebra (over `𝕜`) of double centralizers,
 for which we provide the localized notation `𝓜(𝕜, A)`.  A double centralizer is a pair of
 continuous linear maps `L R : A →L[𝕜] A` satisfying the intertwining condition `R x * y = x * L y`.

diff --git a/src/analysis/normed_space/weak_dual.lean b/src/analysis/normed_space/weak_dual.lean
@@ -10,6 +10,9 @@ import analysis.normed_space.operator_norm
 /-!
 # Weak dual of normed space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `E` be a normed space over a field `𝕜`. This file is concerned with properties of the weak-*
 topology on the dual of `E`. By the dual, we mean either of the type synonyms
 `normed_space.dual 𝕜 E` or `weak_dual 𝕜 E`, depending on whether it is viewed as equipped with its