leanprover-community · github-actions · Jan 18, 2023
diff --git a/src/algebra/gcd_monoid/finset.lean b/src/algebra/gcd_monoid/finset.lean
@@ -9,6 +9,9 @@ import algebra.gcd_monoid.multiset
 /-!
 # GCD and LCM operations on finsets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 - `finset.gcd` - the greatest common denominator of a `finset` of elements of a `gcd_monoid`

diff --git a/src/algebra/hom/centroid.lean b/src/algebra/hom/centroid.lean
@@ -9,6 +9,9 @@ import algebra.hom.group_instances
 /-!
 # Centroid homomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `A` be a (non unital, non associative) algebra. The centroid of `A` is the set of linear maps
 `T` on `A` such that `T` commutes with left and right multiplication, that is to say, for all `a`
 and `b` in `A`,

@@ -8,6 +8,9 @@ import data.finset.card
 /-!
 # Down-compressions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines down-compression.
 
 Down-compressing `𝒜 : finset (finset α)` along `a : α` means removing `a` from the elements of `𝒜`,

diff --git a/src/control/equiv_functor/instances.lean b/src/control/equiv_functor/instances.lean
@@ -9,6 +9,9 @@ import control.equiv_functor
 /-!
 # `equiv_functor` instances
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We derive some `equiv_functor` instances, to enable `equiv_rw` to rewrite under these functions.
 -/
 

diff --git a/src/data/fin/tuple/basic.lean b/src/data/fin/tuple/basic.lean
@@ -10,6 +10,9 @@ import data.set.intervals.basic
 /-!
 # Operation on tuples
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We interpret maps `Π i : fin n, α i` as `n`-tuples of elements of possibly varying type `α i`,
 `(α 0, …, α (n-1))`. A particular case is `fin n → α` of elements with all the same type.
 In this case when `α i` is a constant map, then tuples are isomorphic (but not definitionally equal)

diff --git a/src/data/fin_enum.lean b/src/data/fin_enum.lean
@@ -8,6 +8,9 @@ import data.fintype.basic
 import data.list.prod_sigma
 
 /-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Type class for finitely enumerable types. The property is stronger
 than `fintype` in that it assigns each element a rank in a finite
 enumeration.

diff --git a/src/data/finset/lattice.lean b/src/data/finset/lattice.lean
@@ -11,6 +11,9 @@ import order.complete_lattice
 
 /-!
 # Lattice operations on finsets
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 variables {α β γ ι : Type*}

diff --git a/src/data/finset/n_ary.lean b/src/data/finset/n_ary.lean
@@ -8,6 +8,9 @@ import data.finset.prod
 /-!
 # N-ary images of finsets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `finset.image₂`, the binary image of finsets. This is the finset version of
 `set.image2`. This is mostly useful to define pointwise operations.
 

diff --git a/src/data/finset/nat_antidiagonal.lean b/src/data/finset/nat_antidiagonal.lean
@@ -9,6 +9,9 @@ import data.multiset.nat_antidiagonal
 /-!
 # Antidiagonals in ℕ × ℕ as finsets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the antidiagonals of ℕ × ℕ as finsets: the `n`-th antidiagonal is the finset of
 pairs `(i, j)` such that `i + j = n`. This is useful for polynomial multiplication and more
 generally for sums going from `0` to `n`.

diff --git a/src/data/finset/pairwise.lean b/src/data/finset/pairwise.lean
@@ -8,6 +8,9 @@ import data.finset.lattice
 /-!
 # Relations holding pairwise on finite sets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove a few results about the interaction of `set.pairwise_disjoint` and `finset`,
 as well as the interaction of `list.pairwise disjoint` and the condition of
 `disjoint` on `list.to_finset`, in `set` form.

diff --git a/src/data/finset/powerset.lean b/src/data/finset/powerset.lean
@@ -8,6 +8,9 @@ import data.multiset.powerset
 
 /-!
 # The powerset of a finset
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 namespace finset

diff --git a/src/data/finset/sigma.lean b/src/data/finset/sigma.lean
@@ -9,6 +9,9 @@ import data.set.sigma
 /-!
 # Finite sets in a sigma type
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines a few `finset` constructions on `Σ i, α i`.
 
 ## Main declarations

diff --git a/src/data/fintype/list.lean b/src/data/fintype/list.lean
@@ -10,6 +10,9 @@ import data.finset.powerset
 
 # Fintype instance for nodup lists
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The subtype of `{l : list α // l.nodup}` over a `[fintype α]`
 admits a `fintype` instance.
 

diff --git a/src/data/fintype/sigma.lean b/src/data/fintype/sigma.lean
@@ -9,6 +9,9 @@ import data.finset.sigma
 
 /-!
 # fintype instances for sigma types
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open function

diff --git a/src/data/list/of_fn.lean b/src/data/list/of_fn.lean
@@ -10,6 +10,9 @@ import data.list.join
 /-!
 # Lists from functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Theorems and lemmas for dealing with `list.of_fn`, which converts a function on `fin n` to a list
 of length `n`.
 

diff --git a/src/data/matrix/dmatrix.lean b/src/data/matrix/dmatrix.lean
@@ -8,6 +8,9 @@ import data.fintype.basic
 
 /-!
 # Matrices
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 universes u u' v w z
 

diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
@@ -11,6 +11,9 @@ import data.real.cau_seq_completion
 /-!
 # Real numbers from Cauchy sequences
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `ℝ` as the type of equivalence classes of Cauchy sequences of rational numbers.
 This choice is motivated by how easy it is to prove that `ℝ` is a commutative ring, by simply
 lifting everything to `ℚ`.

diff --git a/src/data/real/sign.lean b/src/data/real/sign.lean
@@ -8,6 +8,9 @@ import data.real.basic
 /-!
 # Real sign function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file introduces and contains some results about `real.sign` which maps negative
 real numbers to -1, positive real numbers to 1, and 0 to 0.
 

diff --git a/src/group_theory/congruence.lean b/src/group_theory/congruence.lean
@@ -11,6 +11,9 @@ import group_theory.submonoid.operations
 /-!
 # Congruence relations
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines congruence relations: equivalence relations that preserve a binary operation,
 which in this case is multiplication or addition. The principal definition is a `structure`
 extending a `setoid` (an equivalence relation), and the inductive definition of the smallest

diff --git a/src/group_theory/perm/support.lean b/src/group_theory/perm/support.lean
@@ -10,6 +10,9 @@ import group_theory.perm.basic
 /-!
 # Support of a permutation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 In the following, `f g : equiv.perm α`.

diff --git a/src/order/grade.lean b/src/order/grade.lean
@@ -9,6 +9,9 @@ import data.int.succ_pred
 /-!
 # Graded orders
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines graded orders, also known as ranked orders.
 
 A `𝕆`-graded order is an order `α` equipped with a distinguished "grade" function `α → 𝕆` which

diff --git a/src/order/hom/bounded.lean b/src/order/hom/bounded.lean
@@ -9,6 +9,9 @@ import order.bounded_order
 /-!
 # Bounded order homomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines (bounded) order homomorphisms.
 
 We use the `fun_like` design, so each type of morphisms has a companion typeclass which is meant to

diff --git a/src/order/sup_indep.lean b/src/order/sup_indep.lean
@@ -10,6 +10,9 @@ import data.fintype.basic
 /-!
 # Supremum independence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define supremum independence of indexed sets. An indexed family `f : ι → α` is
 sup-independent if, for all `a`, `f a` and the supremum of the rest are disjoint.
 

diff --git a/src/ring_theory/congruence.lean b/src/ring_theory/congruence.lean
@@ -12,6 +12,9 @@ import group_theory.congruence
 /-!
 # Congruence relations on rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines congruence relations on rings, which extend `con` and `add_con` on monoids and
 additive monoids.