leanprover-community · github-actions · Mar 20, 2023
diff --git a/src/algebra/dual_number.lean b/src/algebra/dual_number.lean
@@ -9,6 +9,9 @@ import algebra.triv_sq_zero_ext
 /-!
 # Dual numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The dual numbers over `R` are of the form `a + bε`, where `a` and `b` are typically elements of a
 commutative ring `R`, and `ε` is a symbol satisfying `ε^2 = 0`. They are a special case of
 `triv_sq_zero_ext R M` with `M = R`.

diff --git a/src/data/finsupp/well_founded.lean b/src/data/finsupp/well_founded.lean
@@ -9,6 +9,9 @@ import data.finsupp.lex
 /-!
 # Well-foundedness of the lexicographic and product orders on `finsupp`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 `finsupp.lex.well_founded` and the two variants that follow it essentially say that if
 `(>)` is a well order on `α`, `(<)` is well-founded on `N`, and `0` is a bottom element in `N`,
 then the lexicographic `(<)` is well-founded on `α →₀ N`.

diff --git a/src/data/nat/multiplicity.lean b/src/data/nat/multiplicity.lean
@@ -14,6 +14,9 @@ import ring_theory.multiplicity
 /-!
 # Natural number multiplicity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains lemmas about the multiplicity function (the maximum prime power dividing a
 number) when applied to naturals, in particular calculating it for factorials and binomial
 coefficients.

diff --git a/src/data/polynomial/div.lean b/src/data/polynomial/div.lean
@@ -11,6 +11,9 @@ import ring_theory.multiplicity
 /-!
 # Division of univariate polynomials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The main defs are `div_by_monic` and `mod_by_monic`.
 The compatibility between these is given by `mod_by_monic_add_div`.
 We also define `root_multiplicity`.

diff --git a/src/data/zmod/algebra.lean b/src/data/zmod/algebra.lean
@@ -9,6 +9,9 @@ import algebra.algebra.basic
 
 /-!
 # The `zmod n`-algebra structure on rings whose characteristic divides `n`
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 namespace zmod

diff --git a/src/data/zmod/parity.lean b/src/data/zmod/parity.lean
@@ -8,6 +8,9 @@ import data.zmod.basic
 /-!
 # Relating parity to natural numbers mod 2
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module provides lemmas relating `zmod 2` to `even` and `odd`.
 
 ## Tags

diff --git a/src/ring_theory/ideal/idempotent_fg.lean b/src/ring_theory/ideal/idempotent_fg.lean
@@ -8,6 +8,9 @@ import ring_theory.finiteness
 
 /-!
 ## Lemmas on idempotent finitely generated ideals
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 namespace ideal

diff --git a/src/ring_theory/mv_polynomial/symmetric.lean b/src/ring_theory/mv_polynomial/symmetric.lean
@@ -10,6 +10,9 @@ import algebra.algebra.subalgebra.basic
 /-!
 # Symmetric Polynomials and Elementary Symmetric Polynomials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines symmetric `mv_polynomial`s and elementary symmetric `mv_polynomial`s.
 We also prove some basic facts about them.