From 290a7ba01fbcab1b64757bdaa270d28f4dcede35 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <leanprover.community@gmail.com>
Date: Mon, 20 Mar 2023 06:49:15 +0000
Subject: [PATCH] chore(*): add mathlib4 synchronization comments (#18623)

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.dual_number`
* `data.finsupp.well_founded`
* `data.nat.multiplicity`
* `data.polynomial.div`
* `data.zmod.algebra`
* `data.zmod.parity`
* `ring_theory.ideal.idempotent_fg`
* `ring_theory.mv_polynomial.symmetric`
---
 src/algebra/dual_number.lean                 | 3 +++
 src/data/finsupp/well_founded.lean           | 3 +++
 src/data/nat/multiplicity.lean               | 3 +++
 src/data/polynomial/div.lean                 | 3 +++
 src/data/zmod/algebra.lean                   | 3 +++
 src/data/zmod/parity.lean                    | 3 +++
 src/ring_theory/ideal/idempotent_fg.lean     | 3 +++
 src/ring_theory/mv_polynomial/symmetric.lean | 3 +++
 8 files changed, 24 insertions(+)

diff --git a/src/algebra/dual_number.lean b/src/algebra/dual_number.lean
index 9daad87c0525c..31cacf6c8cbeb 100644
--- 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
index a5099ed0ffbf7..9a9450b297ebc 100644
--- 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
index 68a56270c1855..f54f1afac1c5b 100644
--- 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
index 67ab0564bd65b..9abd9e5cf5e15 100644
--- 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
index 7646d996b20cd..65f3f96fc884f 100644
--- 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
index f08e23f86efa9..c83d693c6c394 100644
--- 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
index 029aa6c03d62a..61bdcf8506b19 100644
--- 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
index d3bf7caf12f6b..4922a8cfafbc2 100644
--- 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.