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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.big_operators.finsupp` * `algebra.direct_sum.basic` * `algebra.is_prime_pow` * `combinatorics.set_family.shadow` * `data.dfinsupp.ne_locus` * `data.finsupp.fintype` * `data.finsupp.ne_locus` * `data.fun_like.fintype` * `group_theory.group_action.sub_mul_action.pointwise` * `group_theory.monoid_localization` * `group_theory.subgroup.finite` * `order.filter.modeq` * `order.filter.pointwise` * `ring_theory.subsemiring.basic`
leanprover-community · Jan 31, 2023 · 13a5329 · 13a5329
1 parent ed60ee2
commit 13a5329
Show file tree

Hide file tree

Showing 14 changed files with 42 additions and 0 deletions.
diff --git a/src/algebra/big_operators/finsupp.lean b/src/algebra/big_operators/finsupp.lean
@@ -13,6 +13,9 @@ import group_theory.submonoid.membership
 /-!
 # Big operators for finsupps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains theorems relevant to big operators in finitely supported functions.
 -/
 

diff --git a/src/algebra/direct_sum/basic.lean b/src/algebra/direct_sum/basic.lean
@@ -8,6 +8,9 @@ import group_theory.submonoid.operations
 /-!
 # Direct sum
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the direct sum of abelian groups, indexed by a discrete type.
 
 ## Notation

diff --git a/src/algebra/is_prime_pow.lean b/src/algebra/is_prime_pow.lean
@@ -9,6 +9,9 @@ import number_theory.divisors
 /-!
 # Prime powers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file deals with prime powers: numbers which are positive integer powers of a single prime.
 -/
 

diff --git a/src/combinatorics/set_family/shadow.lean b/src/combinatorics/set_family/shadow.lean
@@ -9,6 +9,9 @@ import logic.function.iterate
 /-!
 # Shadows
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines shadows of a set family. The shadow of a set family is the set family of sets we
 get by removing any element from any set of the original family. If one pictures `finset α` as a big
 hypercube (each dimension being membership of a given element), then taking the shadow corresponds

diff --git a/src/data/dfinsupp/ne_locus.lean b/src/data/dfinsupp/ne_locus.lean
@@ -8,6 +8,9 @@ import data.dfinsupp.basic
 /-!
 # Locus of unequal values of finitely supported dependent functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `N : α → Type*` be a type family, assume that `N a` has a `0` for all `a : α` and let
 `f g : Π₀ a, N a` be finitely supported dependent functions.
 

diff --git a/src/data/finsupp/fintype.lean b/src/data/finsupp/fintype.lean
@@ -10,6 +10,9 @@ import data.fintype.basic
 
 # Finiteness and infiniteness of `finsupp`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Some lemmas on the combination of `finsupp`, `fintype` and `infinite`.
 
 -/

diff --git a/src/data/finsupp/ne_locus.lean b/src/data/finsupp/ne_locus.lean
@@ -8,6 +8,9 @@ import data.finsupp.defs
 /-!
 # Locus of unequal values of finitely supported functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `α N` be two Types, assume that `N` has a `0` and let `f g : α →₀ N` be finitely supported
 functions.
 

diff --git a/src/data/fun_like/fintype.lean b/src/data/fun_like/fintype.lean
@@ -11,6 +11,9 @@ import data.fun_like.basic
 /-!
 # Finiteness of `fun_like` types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show a type `F` with a `fun_like F α β` is finite if both `α` and `β` are finite.
 This corresponds to the following two pairs of declarations:
 

diff --git a/src/group_theory/group_action/sub_mul_action/pointwise.lean b/src/group_theory/group_action/sub_mul_action/pointwise.lean
@@ -9,6 +9,9 @@ import group_theory.group_action.sub_mul_action
 /-!
 # Pointwise monoid structures on sub_mul_action
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides `sub_mul_action.monoid` and weaker typeclasses, which show that `sub_mul_action`s
 inherit the same pointwise multiplications as sets.
 

diff --git a/src/group_theory/monoid_localization.lean b/src/group_theory/monoid_localization.lean
@@ -10,6 +10,9 @@ import algebra.group.units
 /-!
 # Localizations of commutative monoids
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Localizing a commutative ring at one of its submonoids does not rely on the ring's addition, so
 we can generalize localizations to commutative monoids.
 

diff --git a/src/group_theory/subgroup/finite.lean b/src/group_theory/subgroup/finite.lean
@@ -11,6 +11,9 @@ import group_theory.submonoid.membership
 /-!
 # Subgroups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides some result on multiplicative and additive subgroups in the finite context.
 
 ## Tags

diff --git a/src/order/filter/modeq.lean b/src/order/filter/modeq.lean
@@ -9,6 +9,9 @@ import order.filter.at_top_bot
 /-!
 # Numbers are frequently modeq to fixed numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that `m ≡ d [MOD n]` frequently as `m → ∞`.
 -/
 

diff --git a/src/order/filter/pointwise.lean b/src/order/filter/pointwise.lean
@@ -10,6 +10,9 @@ import order.filter.ultrafilter
 /-!
 # Pointwise operations on filters
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines pointwise operations on filters. This is useful because usual algebraic operations
 distribute over pointwise operations. For example,
 * `(f₁ * f₂).map m  = f₁.map m * f₂.map m`

diff --git a/src/ring_theory/subsemiring/basic.lean b/src/ring_theory/subsemiring/basic.lean
@@ -16,6 +16,9 @@ import group_theory.submonoid.membership
 /-!
 # Bundled subsemirings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define bundled subsemirings and some standard constructions: `complete_lattice` structure,
 `subtype` and `inclusion` ring homomorphisms, subsemiring `map`, `comap` and range (`srange`) of
 a `ring_hom` etc.