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

@@ -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`.

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`.

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.

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`.

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

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

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

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.