From ff9a5f7acb7a5e330949c50d706c0d3f85fbe785 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 13 Nov 2024 22:09:06 +0000 Subject: [PATCH] chore: move pointwise set files to `Algebra._.Pointwise` --- Mathlib.lean | 8 ++++---- Mathlib/Algebra/Algebra/Operations.lean | 2 +- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean | 4 ++-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean | 2 +- .../Group/Pointwise/Set}/BigOperators.lean | 0 Mathlib/Algebra/Group/Pointwise/Set/Card.lean | 2 +- .../Pointwise => Algebra/Group/Pointwise/Set}/Finite.lean | 0 .../Group/Pointwise/Set}/ListOfFn.lean | 0 .../Set => Algebra/Order/Group}/Pointwise/Interval.lean | 0 Mathlib/Analysis/Normed/Field/Basic.lean | 4 ++-- Mathlib/Data/Real/Cardinality.lean | 2 +- Mathlib/GroupTheory/Finiteness.lean | 2 +- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean | 2 +- Mathlib/Topology/Algebra/Order/Field.lean | 2 +- Mathlib/Topology/MetricSpace/Pseudo/Real.lean | 2 +- 15 files changed, 16 insertions(+), 16 deletions(-) rename Mathlib/{Data/Set/Pointwise => Algebra/Group/Pointwise/Set}/BigOperators.lean (100%) rename Mathlib/{Data/Set/Pointwise => Algebra/Group/Pointwise/Set}/Finite.lean (100%) rename Mathlib/{Data/Set/Pointwise => Algebra/Group/Pointwise/Set}/ListOfFn.lean (100%) rename Mathlib/{Data/Set => Algebra/Order/Group}/Pointwise/Interval.lean (100%) diff --git a/Mathlib.lean b/Mathlib.lean index 4902e66c634dba..34abebdf62f88f 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -289,7 +289,10 @@ import Mathlib.Algebra.Group.Pi.Lemmas import Mathlib.Algebra.Group.Pointwise.Finset.Basic import Mathlib.Algebra.Group.Pointwise.Finset.Interval import Mathlib.Algebra.Group.Pointwise.Set.Basic +import Mathlib.Algebra.Group.Pointwise.Set.BigOperators import Mathlib.Algebra.Group.Pointwise.Set.Card +import Mathlib.Algebra.Group.Pointwise.Set.Finite +import Mathlib.Algebra.Group.Pointwise.Set.ListOfFn import Mathlib.Algebra.Group.Prod import Mathlib.Algebra.Group.Semiconj.Basic import Mathlib.Algebra.Group.Semiconj.Defs @@ -648,6 +651,7 @@ import Mathlib.Algebra.Order.Group.OrderIso import Mathlib.Algebra.Order.Group.PiLex import Mathlib.Algebra.Order.Group.Pointwise.Bounds import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice +import Mathlib.Algebra.Order.Group.Pointwise.Interval import Mathlib.Algebra.Order.Group.PosPart import Mathlib.Algebra.Order.Group.Prod import Mathlib.Algebra.Order.Group.Synonym @@ -2798,12 +2802,8 @@ import Mathlib.Data.Set.Operations import Mathlib.Data.Set.Opposite import Mathlib.Data.Set.Pairwise.Basic import Mathlib.Data.Set.Pairwise.Lattice -import Mathlib.Data.Set.Pointwise.BigOperators import Mathlib.Data.Set.Pointwise.BoundedMul -import Mathlib.Data.Set.Pointwise.Finite -import Mathlib.Data.Set.Pointwise.Interval import Mathlib.Data.Set.Pointwise.Iterate -import Mathlib.Data.Set.Pointwise.ListOfFn import Mathlib.Data.Set.Pointwise.SMul import Mathlib.Data.Set.Pointwise.Support import Mathlib.Data.Set.Prod diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index 33686a95e9ef48..b39f7aaf5c8b1c 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -6,9 +6,9 @@ Authors: Kenny Lau import Mathlib.Algebra.Algebra.Bilinear import Mathlib.Algebra.Algebra.Opposite import Mathlib.Algebra.Group.Pointwise.Finset.Basic +import Mathlib.Algebra.Group.Pointwise.Set.BigOperators import Mathlib.Algebra.GroupWithZero.NonZeroDivisors import Mathlib.Algebra.Module.Submodule.Pointwise -import Mathlib.Data.Set.Pointwise.BigOperators import Mathlib.Data.Set.Semiring import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean index a7cd803e05c074..7deb89fb1b3813 100644 --- a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean +++ b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean @@ -5,11 +5,11 @@ Authors: Floris van Doorn, Yaël Dillies -/ import Mathlib.Algebra.BigOperators.Group.Finset import Mathlib.Algebra.Group.Action.Pi +import Mathlib.Algebra.Group.Pointwise.Set.Finite import Mathlib.Data.Finset.Density import Mathlib.Data.Finset.Max import Mathlib.Data.Finset.NAry -import Mathlib.Data.Set.Pointwise.Finite -import Mathlib.Data.Set.Pointwise.ListOfFn +import Mathlib.Algebra.Group.Pointwise.Set.ListOfFn import Mathlib.Data.Set.Pointwise.SMul /-! diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean index 479121a3d4a1b9..d06c3e7259b133 100644 --- a/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean +++ b/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ import Mathlib.Algebra.Group.Pointwise.Finset.Basic -import Mathlib.Data.Set.Pointwise.Interval +import Mathlib.Algebra.Order.Group.Pointwise.Interval import Mathlib.Order.Interval.Finset.Defs /-! # Pointwise operations on intervals diff --git a/Mathlib/Data/Set/Pointwise/BigOperators.lean b/Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean similarity index 100% rename from Mathlib/Data/Set/Pointwise/BigOperators.lean rename to Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean diff --git a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean index 80a073b792385c..bb228c7f134f5a 100644 --- a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean +++ b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ -import Mathlib.Data.Set.Pointwise.Finite +import Mathlib.Algebra.Group.Pointwise.Set.Finite import Mathlib.SetTheory.Cardinal.Finite /-! diff --git a/Mathlib/Data/Set/Pointwise/Finite.lean b/Mathlib/Algebra/Group/Pointwise/Set/Finite.lean similarity index 100% rename from Mathlib/Data/Set/Pointwise/Finite.lean rename to Mathlib/Algebra/Group/Pointwise/Set/Finite.lean diff --git a/Mathlib/Data/Set/Pointwise/ListOfFn.lean b/Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean similarity index 100% rename from Mathlib/Data/Set/Pointwise/ListOfFn.lean rename to Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean diff --git a/Mathlib/Data/Set/Pointwise/Interval.lean b/Mathlib/Algebra/Order/Group/Pointwise/Interval.lean similarity index 100% rename from Mathlib/Data/Set/Pointwise/Interval.lean rename to Mathlib/Algebra/Order/Group/Pointwise/Interval.lean diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean index a81ab41393a9d6..eb3c22b61051f6 100644 --- a/Mathlib/Analysis/Normed/Field/Basic.lean +++ b/Mathlib/Analysis/Normed/Field/Basic.lean @@ -5,10 +5,10 @@ Authors: Patrick Massot, Johannes Hölzl -/ import Mathlib.Algebra.Algebra.NonUnitalSubalgebra import Mathlib.Algebra.Algebra.Subalgebra.Basic +import Mathlib.Algebra.Field.Subfield.Defs +import Mathlib.Algebra.Order.Group.Pointwise.Interval import Mathlib.Analysis.Normed.Group.Constructions import Mathlib.Analysis.Normed.Group.Submodule -import Mathlib.Data.Set.Pointwise.Interval -import Mathlib.Algebra.Field.Subfield.Defs /-! # Normed fields diff --git a/Mathlib/Data/Real/Cardinality.lean b/Mathlib/Data/Real/Cardinality.lean index b0a7e99a26fb2d..b41af8e41d56f1 100644 --- a/Mathlib/Data/Real/Cardinality.lean +++ b/Mathlib/Data/Real/Cardinality.lean @@ -3,9 +3,9 @@ Copyright (c) 2019 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ +import Mathlib.Algebra.Order.Group.Pointwise.Interval import Mathlib.Analysis.SpecificLimits.Basic import Mathlib.Data.Rat.Cardinal -import Mathlib.Data.Set.Pointwise.Interval import Mathlib.SetTheory.Cardinal.Continuum /-! diff --git a/Mathlib/GroupTheory/Finiteness.lean b/Mathlib/GroupTheory/Finiteness.lean index 80895c9fc92ee9..bd31d6b8743b43 100644 --- a/Mathlib/GroupTheory/Finiteness.lean +++ b/Mathlib/GroupTheory/Finiteness.lean @@ -3,8 +3,8 @@ Copyright (c) 2021 Riccardo Brasca. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Riccardo Brasca -/ +import Mathlib.Algebra.Group.Pointwise.Set.Finite import Mathlib.Algebra.Group.Subgroup.Pointwise -import Mathlib.Data.Set.Pointwise.Finite import Mathlib.GroupTheory.QuotientGroup.Defs import Mathlib.SetTheory.Cardinal.Finite diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean index 71f99e5c85dde4..259da107ba0114 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean @@ -3,7 +3,7 @@ Copyright (c) 2020 Joseph Myers. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Myers -/ -import Mathlib.Data.Set.Pointwise.Interval +import Mathlib.Algebra.Order.Group.Pointwise.Interval import Mathlib.LinearAlgebra.AffineSpace.Basic import Mathlib.LinearAlgebra.BilinearMap import Mathlib.LinearAlgebra.Pi diff --git a/Mathlib/Topology/Algebra/Order/Field.lean b/Mathlib/Topology/Algebra/Order/Field.lean index 51f7585e7e00c8..ee7ea3caa64425 100644 --- a/Mathlib/Topology/Algebra/Order/Field.lean +++ b/Mathlib/Topology/Algebra/Order/Field.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Benjamin Davidson. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Benjamin Davidson, Devon Tuma, Eric Rodriguez, Oliver Nash -/ -import Mathlib.Data.Set.Pointwise.Interval +import Mathlib.Algebra.Order.Group.Pointwise.Interval import Mathlib.Order.Filter.AtTopBot.Field import Mathlib.Topology.Algebra.Field import Mathlib.Topology.Algebra.Order.Group diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Real.lean b/Mathlib/Topology/MetricSpace/Pseudo/Real.lean index ae477178577c56..baa4f534f75cca 100644 --- a/Mathlib/Topology/MetricSpace/Pseudo/Real.lean +++ b/Mathlib/Topology/MetricSpace/Pseudo/Real.lean @@ -3,7 +3,7 @@ Copyright (c) 2015, 2017 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel -/ -import Mathlib.Data.Set.Pointwise.Interval +import Mathlib.Algebra.Order.Group.Pointwise.Interval import Mathlib.Topology.MetricSpace.Pseudo.Pi /-!