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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.algebra.spectrum`
* `algebra.category.Module.algebra`
* `algebra.lie.free`
* `algebra.lie.normalizer`
* `algebra.lie.quotient`
* `algebra.lie.universal_enveloping`
* `algebra.order.complete_field`
* `algebra.order.interval`
* `algebra.star.order`
* `analysis.normed_space.enorm`
* `analysis.special_functions.integrals`
* `analysis.special_functions.non_integrable`
* `analysis.special_functions.polar_coord`
* `category_theory.monoidal.of_has_finite_products`
* `category_theory.monoidal.opposite`
* `category_theory.monoidal.skeleton`
* `category_theory.monoidal.types.coyoneda`
* `category_theory.preadditive.Mat`
* `data.rat.star`
* `data.real.pi.wallis`
* `field_theory.adjoin`
* `group_theory.schur_zassenhaus`
* `linear_algebra.eigenspace.basic`
* `linear_algebra.tensor_algebra.grading`
* `measure_theory.covering.besicovitch`
* `measure_theory.covering.besicovitch_vector_space`
* `measure_theory.function.jacobian`
* `measure_theory.integral.divergence_theorem`
* `measure_theory.integral.fund_thm_calculus`
* `measure_theory.measure.lebesgue.integral`
* `number_theory.ramification_inertia`
* `ring_theory.dedekind_domain.dvr`
* `ring_theory.dedekind_domain.pid`
* `ring_theory.discrete_valuation_ring.tfae`
* `ring_theory.polynomial.cyclotomic.basic`
* `ring_theory.witt_vector.basic`
* `ring_theory.witt_vector.is_poly`
* `ring_theory.witt_vector.mul_p`
* `ring_theory.witt_vector.teichmuller`
* `topology.algebra.continuous_affine_map`
* `topology.algebra.module.character_space`
* `topology.category.Compactum`
* `topology.continuous_function.units`

src/algebra/algebra/spectrum.lean

@@ -8,6 +8,9 @@ import algebra.star.subalgebra
 import tactic.noncomm_ring
 /-!
 # Spectrum of an element in an algebra
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 This file develops the basic theory of the spectrum of an element of an algebra.
 This theory will serve as the foundation for spectral theory in Banach algebras.
 

src/algebra/category/Module/algebra.lean

@@ -10,6 +10,9 @@ import algebra.category.Module.basic
 /-!
 # Additional typeclass for modules over an algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For an object in `M : Module A`, where `A` is a `k`-algebra,
 we provide additional typeclasses on the underlying type `M`,
 namely `module k M` and `is_scalar_tower k A M`.

src/algebra/lie/free.lean

@@ -11,6 +11,9 @@ import algebra.free_non_unital_non_assoc_algebra
 /-!
 # Free Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a commutative ring `R` and a type `X` we construct the free Lie algebra on `X` with
 coefficients in `R` together with its universal property.
 

src/algebra/lie/normalizer.lean

@@ -10,6 +10,9 @@ import algebra.lie.quotient
 /-!
 # The normalizer of a Lie submodules and subalgebras.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a Lie module `M` over a Lie subalgebra `L`, the normalizer of a Lie submodule `N ⊆ M` is
 the Lie submodule with underlying set `{ m | ∀ (x : L), ⁅x, m⁆ ∈ N }`.
 

src/algebra/lie/quotient.lean

@@ -10,6 +10,9 @@ import linear_algebra.isomorphisms
 /-!
 # Quotients of Lie algebras and Lie modules
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a Lie submodule of a Lie module, the quotient carries a natural Lie module structure. In the
 special case that the Lie module is the Lie algebra itself via the adjoint action, the submodule
 is a Lie ideal and the quotient carries a natural Lie algebra structure.

src/algebra/lie/universal_enveloping.lean

@@ -10,6 +10,9 @@ import linear_algebra.tensor_algebra.basic
 /-!
 # Universal enveloping algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a commutative ring `R` and a Lie algebra `L` over `R`, we construct the universal
 enveloping algebra of `L`, together with its universal property.
 

src/algebra/order/complete_field.lean

@@ -10,6 +10,9 @@ import analysis.special_functions.pow.real
 /-!
 # Conditionally complete linear ordered fields
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file shows that the reals are unique, or, more formally, given a type satisfying the common
 axioms of the reals (field, conditionally complete, linearly ordered) that there is an isomorphism
 preserving these properties to the reals. This is `rat.induced_order_ring_iso`. Moreover this

src/algebra/order/interval.lean

@@ -13,6 +13,9 @@ import tactic.positivity
 /-!
 # Interval arithmetic
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines arithmetic operations on intervals and prove their correctness. Note that this is
 full precision operations. The essentials of float operations can be found
 in `data.fp.basic`. We have not yet integrated these with the rest of the library.

src/algebra/star/order.lean

@@ -9,6 +9,9 @@ import group_theory.submonoid.basic
 
 /-! # Star ordered rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the class `star_ordered_ring R`, which says that the order on `R` respects the
 star operation, i.e. an element `r` is nonnegative iff it is in the `add_submonoid` generated by
 elements of the form `star s * s`. In many cases, including all C⋆-algebras, this can be reduced to

src/analysis/normed_space/enorm.lean

@@ -8,6 +8,9 @@ import analysis.normed_space.basic
 /-!
 # Extended norm
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define a structure `enorm 𝕜 V` representing an extended norm (i.e., a norm that can
 take the value `∞`) on a vector space `V` over a normed field `𝕜`. We do not use `class` for
 an `enorm` because the same space can have more than one extended norm. For example, the space of

src/analysis/special_functions/integrals.lean

@@ -9,6 +9,9 @@ import analysis.special_functions.trigonometric.arctan_deriv
 /-!
 # Integration of specific interval integrals
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains proofs of the integrals of various specific functions. This includes:
 * Integrals of simple functions, such as `id`, `pow`, `inv`, `exp`, `log`
 * Integrals of some trigonometric functions, such as `sin`, `cos`, `1 / (1 + x^2)`

src/analysis/special_functions/non_integrable.lean

@@ -9,6 +9,9 @@ import measure_theory.integral.fund_thm_calculus
 /-!
 # Non integrable 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 derivative of a function that tends to infinity is not interval
 integrable, see `interval_integral.not_integrable_has_deriv_at_of_tendsto_norm_at_top_filter` and
 `interval_integral.not_integrable_has_deriv_at_of_tendsto_norm_at_top_punctured`.  Then we apply the

src/analysis/special_functions/polar_coord.lean

@@ -9,6 +9,9 @@ import measure_theory.function.jacobian
 /-!
 # Polar coordinates
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define polar coordinates, as a local homeomorphism in `ℝ^2` between `ℝ^2 - (-∞, 0]` and
 `(0, +∞) × (-π, π)`. Its inverse is given by `(r, θ) ↦ (r cos θ, r sin θ)`.
 

src/category_theory/monoidal/of_has_finite_products.lean

@@ -10,6 +10,9 @@ import category_theory.limits.shapes.terminal
 /-!
 # The natural monoidal structure on any category with finite (co)products.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A category with a monoidal structure provided in this way
 is sometimes called a (co)cartesian category,
 although this is also sometimes used to mean a finitely complete category.

src/category_theory/monoidal/opposite.lean

@@ -8,6 +8,9 @@ import category_theory.monoidal.coherence
 /-!
 # Monoidal opposites
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We write `Cᵐᵒᵖ` for the monoidal opposite of a monoidal category `C`.
 -/
 

src/category_theory/monoidal/skeleton.lean

@@ -10,6 +10,9 @@ import category_theory.skeletal
 /-!
 # The monoid on the skeleton of a monoidal category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The skeleton of a monoidal category is a monoid.
 -/
 

src/category_theory/monoidal/types/coyoneda.lean

@@ -8,6 +8,9 @@ import category_theory.monoidal.coherence_lemmas
 
 /-!
 # `(𝟙_ C ⟶ -)` is a lax monoidal functor to `Type`
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open category_theory

src/category_theory/preadditive/Mat.lean

@@ -17,6 +17,9 @@ import algebra.opposites
 /-!
 # Matrices over a category.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When `C` is a preadditive category, `Mat_ C` is the preadditive category
 whose objects are finite tuples of objects in `C`, and
 whose morphisms are matrices of morphisms from `C`.

src/data/rat/star.lean

@@ -10,6 +10,9 @@ import group_theory.submonoid.membership
 
 /-! # Star order structure on ℚ
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Here we put the trivial `star` operation on `ℚ` for convenience and show that it is a
 `star_ordered_ring`. In particular, this means that every element of `ℚ` is a sum of squares.
 -/

src/data/real/pi/wallis.lean

@@ -7,6 +7,9 @@ import analysis.special_functions.integrals
 
 /-! # The Wallis formula for Pi
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file establishes the Wallis product for `π` (`real.tendsto_prod_pi_div_two`). Our proof is
 largely about analyzing the behaviour of the sequence `∫ x in 0..π, sin x ^ n` as `n → ∞`.
 See: https://en.wikipedia.org/wiki/Wallis_product

src/field_theory/adjoin.lean

@@ -12,6 +12,9 @@ import ring_theory.tensor_product
 /-!
 # Adjoining Elements to Fields
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we introduce the notion of adjoining elements to fields.
 This isn't quite the same as adjoining elements to rings.
 For example, `algebra.adjoin K {x}` might not include `x⁻¹`.

src/group_theory/schur_zassenhaus.lean

@@ -10,6 +10,9 @@ import group_theory.transfer
 /-!
 # The Schur-Zassenhaus Theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the Schur-Zassenhaus theorem.
 
 ## Main results

src/linear_algebra/eigenspace/basic.lean

@@ -12,6 +12,9 @@ import linear_algebra.finite_dimensional
 /-!
 # Eigenvectors and eigenvalues
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines eigenspaces, eigenvalues, and eigenvalues, as well as their generalized
 counterparts. We follow Axler's approach [axler2015] because it allows us to derive many properties
 without choosing a basis and without using matrices.

src/linear_algebra/tensor_algebra/grading.lean

@@ -9,6 +9,9 @@ import ring_theory.graded_algebra.basic
 /-!
 # Results about the grading structure of the tensor algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The main result is `tensor_algebra.graded_algebra`, which says that the tensor algebra is a
 ℕ-graded algebra.
 -/

src/measure_theory/covering/besicovitch.lean

@@ -13,6 +13,9 @@ import topology.metric_space.basic
 /-!
 # Besicovitch covering theorems
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The topological Besicovitch covering theorem ensures that, in a nice metric space, there exists a
 number `N` such that, from any family of balls with bounded radii, one can extract `N` families,
 each made of disjoint balls, covering together all the centers of the initial family.

src/measure_theory/covering/besicovitch_vector_space.lean

@@ -10,6 +10,9 @@ import measure_theory.covering.besicovitch
 /-!
 # Satellite configurations for Besicovitch covering lemma in vector spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The Besicovitch covering theorem ensures that, in a nice metric space, there exists a number `N`
 such that, from any family of balls with bounded radii, one can extract `N` families, each made of
 disjoint balls, covering together all the centers of the initial family.

src/measure_theory/function/jacobian.lean

@@ -13,6 +13,9 @@ import measure_theory.constructions.polish
 /-!
 # Change of variables in higher-dimensional integrals
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `μ` be a Lebesgue measure on a finite-dimensional real vector space `E`.
 Let `f : E → E` be a function which is injective and differentiable on a measurable set `s`,
 with derivative `f'`. Then we prove that `f '' s` is measurable, and

src/measure_theory/integral/divergence_theorem.lean

@@ -12,6 +12,9 @@ import measure_theory.integral.interval_integral
 /-!
 # Divergence theorem for Bochner integral
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the Divergence theorem for Bochner integral on a box in
 `ℝⁿ⁺¹ = fin (n + 1) → ℝ`. More precisely, we prove the following theorem.
 

src/measure_theory/integral/fund_thm_calculus.lean

@@ -15,6 +15,9 @@ import measure_theory.integral.vitali_caratheodory
 /-!
 # Fundamental Theorem of Calculus
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove various versions of the
 [fundamental theorem of calculus](https://en.wikipedia.org/wiki/Fundamental_theorem_of_calculus)
 for interval integrals in `ℝ`.

src/measure_theory/measure/lebesgue/integral.lean

@@ -6,7 +6,10 @@ Authors: Johannes Hölzl, Sébastien Gouëzel, Yury Kudryashov
 import measure_theory.integral.set_integral
 import measure_theory.measure.lebesgue.basic
 
-/-! # Properties of integration with respect to the Lebesgue measure -/
+/-! # Properties of integration with respect to the Lebesgue measure 
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.-/
 
 open set filter measure_theory measure_theory.measure topological_space
 

src/number_theory/ramification_inertia.lean

@@ -10,6 +10,9 @@ import ring_theory.dedekind_domain.ideal
 /-!
 # Ramification index and inertia degree
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given `P : ideal S` lying over `p : ideal R` for the ring extension `f : R →+* S`
 (assuming `P` and `p` are prime or maximal where needed),
 the **ramification index** `ideal.ramification_idx f p P` is the multiplicity of `P` in `map f p`,

src/ring_theory/dedekind_domain/dvr.lean

@@ -10,6 +10,9 @@ import ring_theory.discrete_valuation_ring.tfae
 /-!
 # Dedekind domains
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines an equivalent notion of a Dedekind domain (or Dedekind ring),
 namely a Noetherian integral domain where the localization at all nonzero prime ideals is a DVR
 (TODO: and shows that implies the main definition).

src/ring_theory/dedekind_domain/pid.lean

@@ -10,6 +10,9 @@ import ring_theory.dedekind_domain.ideal
 /-!
 # Proving a Dedekind domain is a PID
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains some results that we can use to show all ideals in a Dedekind domain are
 principal.
 

src/ring_theory/discrete_valuation_ring/tfae.lean

@@ -12,6 +12,9 @@ import ring_theory.nakayama
 
 # Equivalent conditions for DVR
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In `discrete_valuation_ring.tfae`, we show that the following are equivalent for a
 noetherian local domain `(R, m, k)`:
 - `R` is a discrete valuation ring

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -18,6 +18,9 @@ import ring_theory.roots_of_unity.basic
 /-!
 # Cyclotomic polynomials.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For `n : ℕ` and an integral domain `R`, we define a modified version of the `n`-th cyclotomic
 polynomial with coefficients in `R`, denoted `cyclotomic' n R`, as `∏ (X - μ)`, where `μ` varies
 over the primitive `n`th roots of unity. If there is a primitive `n`th root of unity in `R` then

src/ring_theory/witt_vector/basic.lean

@@ -11,6 +11,9 @@ import ring_theory.witt_vector.defs
 /-!
 # Witt vectors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file verifies that the ring operations on `witt_vector p R`
 satisfy the axioms of a commutative ring.
 

src/ring_theory/witt_vector/is_poly.lean

@@ -11,6 +11,9 @@ import data.mv_polynomial.funext
 /-!
 # The `is_poly` predicate
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 `witt_vector.is_poly` is a (type-valued) predicate on functions `f : Π R, 𝕎 R → 𝕎 R`.
 It asserts that there is a family of polynomials `φ : ℕ → mv_polynomial ℕ ℤ`,
 such that the `n`th coefficient of `f x` is equal to `φ n` evaluated on the coefficients of `x`.

src/ring_theory/witt_vector/mul_p.lean

@@ -9,6 +9,9 @@ import ring_theory.witt_vector.is_poly
 /-!
 ## Multiplication by `n` in the ring of Witt vectors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we show that multiplication by `n` in the ring of Witt vectors
 is a polynomial function. We then use this fact to show that the composition of Frobenius
 and Verschiebung is equal to multiplication by `p`.

src/ring_theory/witt_vector/teichmuller.lean

@@ -9,6 +9,9 @@ import ring_theory.witt_vector.basic
 /-!
 # Teichmüller lifts
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `witt_vector.teichmuller`, a monoid hom `R →* 𝕎 R`, which embeds `r : R` as the
 `0`-th component of a Witt vector whose other coefficients are `0`.