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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.group.semiconj`: leanprover-community/mathlib4#717
* `algebra.group_with_zero.basic`: leanprover-community/mathlib4#669
* `algebra.group_with_zero.inj_surj`: leanprover-community/mathlib4#722
* `algebra.ring.inj_surj`: leanprover-community/mathlib4#734
* `algebra.ring.units`: leanprover-community/mathlib4#746
* `data.finite.defs`: leanprover-community/mathlib4#698
* `order.lattice`: leanprover-community/mathlib4#642

src/algebra/group/semiconj.lean

@@ -10,6 +10,10 @@ import algebra.group.units
 /-!
 # Semiconjugate elements of a semigroup
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/717
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 We say that `x` is semiconjugate to `y` by `a` (`semiconj_by a x y`), if `a * x = y * a`.

src/algebra/group_with_zero/basic.lean

@@ -10,6 +10,10 @@ import algebra.group.order_synonym
 /-!
 # Groups with an adjoined zero element
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/669
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file describes structures that are not usually studied on their own right in mathematics,
 namely a special sort of monoid: apart from a distinguished “zero element” they form a group,
 or in other words, they are groups with an adjoined zero element.

src/algebra/group_with_zero/inj_surj.lean

@@ -9,6 +9,9 @@ import algebra.group_with_zero.defs
 /-!
 # Lifting groups with zero along injective/surjective maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/722
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open function

src/algebra/ring/inj_surj.lean

@@ -10,6 +10,9 @@ import algebra.group_with_zero.inj_surj
 /-!
 # Pulling back rings along injective maps, and pushing them forward along surjective maps.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/734
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {R : Type x}

src/algebra/ring/units.lean

@@ -9,6 +9,9 @@ import algebra.group.units
 /-!
 # Units in semirings and rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/746
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {R : Type x}

src/data/finite/defs.lean

@@ -8,6 +8,10 @@ import logic.equiv.basic
 /-!
 # Definition of the `finite` typeclass
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/698
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines a typeclass `finite` saying that `α : Sort*` is finite. A type is `finite` if it
 is equivalent to `fin n` for some `n`. We also define `infinite α` as a typeclass equivalent to
 `¬finite α`.

src/order/lattice.lean

@@ -10,6 +10,10 @@ import tactic.pi_instances
 /-!
 # (Semi-)lattices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/642
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Semilattices are partially ordered sets with join (greatest lower bound, or `sup`) or
 meet (least upper bound, or `inf`) operations. Lattices are posets that are both
 join-semilattices and meet-semilattices.