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

github-actions[bot] · github-actions[bot] · commit 1fc36cc9c826 · 2022-11-28T03:03:16.000Z
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
diff --git a/src/algebra/group/semiconj.lean b/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`.
diff --git a/src/algebra/group_with_zero/basic.lean b/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.
diff --git a/src/algebra/group_with_zero/inj_surj.lean b/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
diff --git a/src/algebra/ring/inj_surj.lean b/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}
diff --git a/src/algebra/ring/units.lean b/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}
diff --git a/src/data/finite/defs.lean b/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 α`.
diff --git a/src/order/lattice.lean b/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.
