From 13a5329a8625701af92e9a96ffc90fa787fff24d Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Tue, 31 Jan 2023 13:11:30 +0000 Subject: [PATCH] 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` --- src/algebra/big_operators/finsupp.lean | 3 +++ src/algebra/direct_sum/basic.lean | 3 +++ src/algebra/is_prime_pow.lean | 3 +++ src/combinatorics/set_family/shadow.lean | 3 +++ src/data/dfinsupp/ne_locus.lean | 3 +++ src/data/finsupp/fintype.lean | 3 +++ src/data/finsupp/ne_locus.lean | 3 +++ src/data/fun_like/fintype.lean | 3 +++ src/group_theory/group_action/sub_mul_action/pointwise.lean | 3 +++ src/group_theory/monoid_localization.lean | 3 +++ src/group_theory/subgroup/finite.lean | 3 +++ src/order/filter/modeq.lean | 3 +++ src/order/filter/pointwise.lean | 3 +++ src/ring_theory/subsemiring/basic.lean | 3 +++ 14 files changed, 42 insertions(+) diff --git a/src/algebra/big_operators/finsupp.lean b/src/algebra/big_operators/finsupp.lean index ded7e78f17f9f..456f1fd9dcb51 100644 --- 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 index 0b14312f4daea..181c4a6c7f016 100644 --- 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 index 862dd75df9797..790f67bedab9b 100644 --- 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 index 7471273e79fb1..f02c1165296ea 100644 --- 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 index 3d50a0f83d23a..772d04af470e8 100644 --- 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 index 0f77c4113b1dd..9f776641e39f0 100644 --- 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 index 39b84a7643a10..3a37840ccb78e 100644 --- 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 index 64f0b9e8732f8..168b503062b7b 100644 --- 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 index 3c233120b93d5..e54d5c31913a0 100644 --- 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 index 2a89add0d748b..20c82192d58bb 100644 --- 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 index b8de0c882f0db..a5ab6c826172f 100644 --- 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 index 94fee945148c6..015caefbdf3fe 100644 --- 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 index 4c4dca90e03fc..f9355b3a67674 100644 --- 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 index 7fad17093710a..f06b9c51eff95 100644 --- 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.