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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.gcd_monoid.basic` * `data.bundle` * `data.pnat.prime` * `data.rat.cast` * `data.set.intervals.monotone` * `group_theory.group_action.embedding` * `group_theory.submonoid.center` * `group_theory.submonoid.centralizer` * `group_theory.submonoid.operations` * `group_theory.subsemigroup.membership` * `order.extension.linear` * `order.monotone.monovary` * `order.succ_pred.limit`
leanprover-community · Jan 5, 2023 · baba818 · baba818
1 parent 50088c9
commit baba818
Show file tree

Hide file tree

Showing 13 changed files with 39 additions and 0 deletions.
diff --git a/src/algebra/gcd_monoid/basic.lean b/src/algebra/gcd_monoid/basic.lean
@@ -11,6 +11,9 @@ import algebra.ring.regular
 /-!
 # Monoids with normalization functions, `gcd`, and `lcm`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines extra structures on `cancel_comm_monoid_with_zero`s, including `is_domain`s.
 
 ## Main Definitions

diff --git a/src/data/bundle.lean b/src/data/bundle.lean
@@ -7,6 +7,9 @@ import algebra.module.basic
 
 /-!
 # Bundle
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Basic data structure to implement fiber bundles, vector bundles (maybe fibrations?), etc. This file
 should contain all possible results that do not involve any topology.
 

diff --git a/src/data/pnat/prime.lean b/src/data/pnat/prime.lean
@@ -9,6 +9,9 @@ import data.pnat.basic
 /-!
 # Primality and GCD on pnat
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file extends the theory of `ℕ+` with `gcd`, `lcm` and `prime` functions, analogous to those on
 `nat`.
 -/

diff --git a/src/data/rat/cast.lean b/src/data/rat/cast.lean
@@ -13,6 +13,9 @@ import algebra.order.field.basic
 /-!
 # Casts for Rational Numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Summary
 
 We define the canonical injection from ℚ into an arbitrary division ring and prove various

diff --git a/src/data/set/intervals/monotone.lean b/src/data/set/intervals/monotone.lean
@@ -9,6 +9,9 @@ import order.succ_pred.basic
 /-!
 # Monotonicity on intervals
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that `set.Ici` etc are monotone/antitone functions. We also prove some lemmas
 about functions monotone on intervals in `succ_order`s.
 -/

diff --git a/src/group_theory/group_action/embedding.lean b/src/group_theory/group_action/embedding.lean
@@ -9,6 +9,9 @@ import group_theory.group_action.pi
 /-!
 # Group actions on embeddings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides a `mul_action G (α ↪ β)` instance that agrees with the `mul_action G (α → β)`
 instances defined by `pi.mul_action`.
 

diff --git a/src/group_theory/submonoid/center.lean b/src/group_theory/submonoid/center.lean
@@ -9,6 +9,9 @@ import group_theory.subsemigroup.center
 /-!
 # Centers of monoids
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 * `submonoid.center`: the center of a monoid

diff --git a/src/group_theory/submonoid/centralizer.lean b/src/group_theory/submonoid/centralizer.lean
@@ -9,6 +9,9 @@ import group_theory.submonoid.center
 /-!
 # Centralizers of magmas and monoids
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 * `submonoid.centralizer`: the centralizer of a subset of a monoid

diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean
@@ -12,6 +12,9 @@ import group_theory.subsemigroup.operations
 /-!
 # Operations on `submonoid`s
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define various operations on `submonoid`s and `monoid_hom`s.
 
 ## Main definitions

diff --git a/src/group_theory/subsemigroup/membership.lean b/src/group_theory/subsemigroup/membership.lean
@@ -8,6 +8,9 @@ import group_theory.subsemigroup.basic
 /-!
 # Subsemigroups: membership criteria
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove various facts about membership in a subsemigroup.
 The intent is to mimic `group_theory/submonoid/membership`, but currently this file is mostly a
 stub and only provides rudimentary support.

diff --git a/src/order/extension/linear.lean b/src/order/extension/linear.lean
@@ -9,6 +9,9 @@ import tactic.by_contra
 /-!
 # Extend a partial order to a linear order
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file constructs a linear order which is an extension of the given partial order, using Zorn's
 lemma.
 -/

diff --git a/src/order/monotone/monovary.lean b/src/order/monotone/monovary.lean
@@ -8,6 +8,9 @@ import data.set.image
 /-!
 # Monovariance of functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Two functions *vary together* if a strict change in the first implies a change in the second.
 
 This is in some sense a way to say that two functions `f : ι → α`, `g : ι → β` are "monotone

diff --git a/src/order/succ_pred/limit.lean b/src/order/succ_pred/limit.lean
@@ -9,6 +9,9 @@ import order.succ_pred.basic
 /-!
 # Successor and predecessor limits
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the predicate `order.is_succ_limit` for "successor limits", values that don't cover any
 others. They are so named since they can't be the successors of anything smaller. We define
 `order.is_pred_limit` analogously, and prove basic results.