From 783b6bc9b8985c33ebb3f699094f4931b205e956 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 29 Mar 2024 09:13:20 +0000 Subject: [PATCH] move(RCLike): Move out of `Data` (#11753) `RCLike` is an analytic typeclass, hence should be under `Analysis` --- Mathlib.lean | 4 ++-- Mathlib/Analysis/Calculus/MeanValue.lean | 2 +- Mathlib/Analysis/Complex/Basic.lean | 2 +- Mathlib/Analysis/Complex/Tietze.lean | 2 +- Mathlib/Analysis/Convex/Gauge.lean | 2 +- Mathlib/Analysis/InnerProductSpace/Projection.lean | 2 +- Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean | 2 +- Mathlib/Analysis/Normed/Group/Tannery.lean | 2 +- Mathlib/Analysis/NormedSpace/Extend.lean | 2 +- Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean | 2 +- Mathlib/Analysis/NormedSpace/RCLike.lean | 2 +- Mathlib/Analysis/NormedSpace/Star/Matrix.lean | 2 +- Mathlib/{Data => Analysis}/RCLike/Basic.lean | 0 Mathlib/{Data => Analysis}/RCLike/Lemmas.lean | 2 +- Mathlib/Analysis/SpecificLimits/RCLike.lean | 2 +- Mathlib/Data/Real/Sqrt.lean | 2 +- Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean | 2 +- Mathlib/MeasureTheory/Function/L2Space.lean | 2 +- Mathlib/MeasureTheory/Function/SpecialFunctions/RCLike.lean | 2 +- Mathlib/NumberTheory/SumPrimeReciprocals.lean | 2 +- Mathlib/Topology/ContinuousFunction/Ideals.lean | 2 +- Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean | 2 +- 22 files changed, 22 insertions(+), 22 deletions(-) rename Mathlib/{Data => Analysis}/RCLike/Basic.lean (100%) rename Mathlib/{Data => Analysis}/RCLike/Lemmas.lean (98%) diff --git a/Mathlib.lean b/Mathlib.lean index 7fe9457f66647..c1659953f522b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -936,6 +936,8 @@ import Mathlib.Analysis.ODE.Gronwall import Mathlib.Analysis.ODE.PicardLindelof import Mathlib.Analysis.PSeries import Mathlib.Analysis.Quaternion +import Mathlib.Analysis.RCLike.Basic +import Mathlib.Analysis.RCLike.Lemmas import Mathlib.Analysis.Seminorm import Mathlib.Analysis.SpecialFunctions.Arsinh import Mathlib.Analysis.SpecialFunctions.Bernstein @@ -2029,8 +2031,6 @@ import Mathlib.Data.QPF.Multivariate.Constructions.Quot import Mathlib.Data.QPF.Multivariate.Constructions.Sigma import Mathlib.Data.QPF.Univariate.Basic import Mathlib.Data.Quot -import Mathlib.Data.RCLike.Basic -import Mathlib.Data.RCLike.Lemmas import Mathlib.Data.Rat.BigOperators import Mathlib.Data.Rat.Cast.CharZero import Mathlib.Data.Rat.Cast.Defs diff --git a/Mathlib/Analysis/Calculus/MeanValue.lean b/Mathlib/Analysis/Calculus/MeanValue.lean index 6f048296c0439..7f910f9c26f2b 100644 --- a/Mathlib/Analysis/Calculus/MeanValue.lean +++ b/Mathlib/Analysis/Calculus/MeanValue.lean @@ -9,7 +9,7 @@ import Mathlib.Analysis.Calculus.Deriv.Mul import Mathlib.Analysis.Calculus.Deriv.Comp import Mathlib.Analysis.Calculus.LocalExtr.Rolle import Mathlib.Analysis.Convex.Normed -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic #align_import analysis.calculus.mean_value from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe" diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean index d5de8d04e751d..79d2765734c5f 100644 --- a/Mathlib/Analysis/Complex/Basic.lean +++ b/Mathlib/Analysis/Complex/Basic.lean @@ -6,7 +6,7 @@ Authors: Sébastien Gouëzel import Mathlib.Data.Complex.Module import Mathlib.Data.Complex.Order import Mathlib.Data.Complex.Exponential -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic import Mathlib.Topology.Algebra.InfiniteSum.Module import Mathlib.Topology.Instances.RealVectorSpace diff --git a/Mathlib/Analysis/Complex/Tietze.lean b/Mathlib/Analysis/Complex/Tietze.lean index 03c8e734e6cc8..ec98170bc12fb 100644 --- a/Mathlib/Analysis/Complex/Tietze.lean +++ b/Mathlib/Analysis/Complex/Tietze.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jireh Loreaux -/ import Mathlib.Analysis.Complex.Basic -import Mathlib.Data.RCLike.Lemmas +import Mathlib.Analysis.RCLike.Lemmas import Mathlib.Topology.TietzeExtension import Mathlib.Analysis.NormedSpace.HomeomorphBall import Mathlib.Analysis.NormedSpace.RCLike diff --git a/Mathlib/Analysis/Convex/Gauge.lean b/Mathlib/Analysis/Convex/Gauge.lean index eaa33eccff6ff..221d69120abea 100644 --- a/Mathlib/Analysis/Convex/Gauge.lean +++ b/Mathlib/Analysis/Convex/Gauge.lean @@ -7,7 +7,7 @@ import Mathlib.Analysis.Convex.Topology import Mathlib.Analysis.NormedSpace.Pointwise import Mathlib.Analysis.Seminorm import Mathlib.Analysis.LocallyConvex.Bounded -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic #align_import analysis.convex.gauge from "leanprover-community/mathlib"@"373b03b5b9d0486534edbe94747f23cb3712f93d" diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index 15dc419faa505..0645ed5c1d26c 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -7,7 +7,7 @@ import Mathlib.Analysis.Convex.Basic import Mathlib.Analysis.InnerProductSpace.Orthogonal import Mathlib.Analysis.InnerProductSpace.Symmetric import Mathlib.Analysis.NormedSpace.RCLike -import Mathlib.Data.RCLike.Lemmas +import Mathlib.Analysis.RCLike.Lemmas import Mathlib.Algebra.DirectSum.Decomposition #align_import analysis.inner_product_space.projection from "leanprover-community/mathlib"@"0b7c740e25651db0ba63648fbae9f9d6f941e31b" diff --git a/Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean b/Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean index 01880d20609ab..cc264111fe42e 100644 --- a/Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean +++ b/Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Doll -/ import Mathlib.Analysis.LocallyConvex.Bounded -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic #align_import analysis.locally_convex.continuous_of_bounded from "leanprover-community/mathlib"@"3f655f5297b030a87d641ad4e825af8d9679eb0b" diff --git a/Mathlib/Analysis/Normed/Group/Tannery.lean b/Mathlib/Analysis/Normed/Group/Tannery.lean index 0771fe1326ba0..8afac11f7c0d8 100644 --- a/Mathlib/Analysis/Normed/Group/Tannery.lean +++ b/Mathlib/Analysis/Normed/Group/Tannery.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: David Loeffler -/ -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic import Mathlib.Analysis.Normed.Group.InfiniteSum /-! diff --git a/Mathlib/Analysis/NormedSpace/Extend.lean b/Mathlib/Analysis/NormedSpace/Extend.lean index a09e2b92b43ef..1edadb078c539 100644 --- a/Mathlib/Analysis/NormedSpace/Extend.lean +++ b/Mathlib/Analysis/NormedSpace/Extend.lean @@ -5,7 +5,7 @@ Authors: Ruben Van de Velde -/ import Mathlib.Algebra.Algebra.RestrictScalars import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic #align_import analysis.normed_space.extend from "leanprover-community/mathlib"@"3f655f5297b030a87d641ad4e825af8d9679eb0b" diff --git a/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean b/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean index 6d02d6bc48dd8..309cbe8b8e38c 100644 --- a/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean +++ b/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean @@ -6,7 +6,7 @@ Authors: Yury Kudryashov, Heather Macbeth import Mathlib.Analysis.Convex.Cone.Extension import Mathlib.Analysis.NormedSpace.RCLike import Mathlib.Analysis.NormedSpace.Extend -import Mathlib.Data.RCLike.Lemmas +import Mathlib.Analysis.RCLike.Lemmas #align_import analysis.normed_space.hahn_banach.extension from "leanprover-community/mathlib"@"915591b2bb3ea303648db07284a161a7f2a9e3d4" diff --git a/Mathlib/Analysis/NormedSpace/RCLike.lean b/Mathlib/Analysis/NormedSpace/RCLike.lean index a665888a4c3e8..357505d65fcbb 100644 --- a/Mathlib/Analysis/NormedSpace/RCLike.lean +++ b/Mathlib/Analysis/NormedSpace/RCLike.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Kalle Kytölä. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kalle Kytölä -/ -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic import Mathlib.Analysis.NormedSpace.Pointwise diff --git a/Mathlib/Analysis/NormedSpace/Star/Matrix.lean b/Mathlib/Analysis/NormedSpace/Star/Matrix.lean index 8a1bbdacd8a24..0c2476723eaa0 100644 --- a/Mathlib/Analysis/NormedSpace/Star/Matrix.lean +++ b/Mathlib/Analysis/NormedSpace/Star/Matrix.lean @@ -5,7 +5,7 @@ Authors: Hans Parshall -/ import Mathlib.Analysis.InnerProductSpace.Adjoint import Mathlib.Analysis.Matrix -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic import Mathlib.LinearAlgebra.UnitaryGroup import Mathlib.Topology.UniformSpace.Matrix diff --git a/Mathlib/Data/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean similarity index 100% rename from Mathlib/Data/RCLike/Basic.lean rename to Mathlib/Analysis/RCLike/Basic.lean diff --git a/Mathlib/Data/RCLike/Lemmas.lean b/Mathlib/Analysis/RCLike/Lemmas.lean similarity index 98% rename from Mathlib/Data/RCLike/Lemmas.lean rename to Mathlib/Analysis/RCLike/Lemmas.lean index 2bb785c410bb6..cba461c1d4706 100644 --- a/Mathlib/Data/RCLike/Lemmas.lean +++ b/Mathlib/Analysis/RCLike/Lemmas.lean @@ -5,7 +5,7 @@ Authors: Frédéric Dupuis -/ import Mathlib.Analysis.NormedSpace.FiniteDimension import Mathlib.FieldTheory.Tower -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic #align_import data.is_R_or_C.lemmas from "leanprover-community/mathlib"@"468b141b14016d54b479eb7a0fff1e360b7e3cf6" diff --git a/Mathlib/Analysis/SpecificLimits/RCLike.lean b/Mathlib/Analysis/SpecificLimits/RCLike.lean index a78ce5b36914d..ff35c8a982a7d 100644 --- a/Mathlib/Analysis/SpecificLimits/RCLike.lean +++ b/Mathlib/Analysis/SpecificLimits/RCLike.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Xavier Généreux, Patrick Massot -/ import Mathlib.Analysis.SpecificLimits.Basic -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic /-! # A collection of specific limit computations for `RCLike` diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean index b782cea35664f..8d18748cd4fa9 100644 --- a/Mathlib/Data/Real/Sqrt.lean +++ b/Mathlib/Data/Real/Sqrt.lean @@ -483,7 +483,7 @@ theorem sqrt_one_add_le (h : -1 ≤ x) : sqrt (1 + x) ≤ 1 + x / 2 := by `ComplexOrder` scope because currently the order on `ℂ` is not enabled globally. But we want `StarOrderedRing ℝ` to be available globally, so we include this instance separately. In addition, providing this instance here makes it available earlier in the import -hierarchy; otherwise in order to access it we would need to import `Data.RCLike.Basic` -/ +hierarchy; otherwise in order to access it we would need to import `Analysis.RCLike.Basic` -/ instance : StarOrderedRing ℝ := StarOrderedRing.ofNonnegIff' add_le_add_left fun r => by refine ⟨fun hr => ⟨sqrt r, (mul_self_sqrt hr).symm⟩, ?_⟩ diff --git a/Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean b/Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean index 78970f8baf2b0..38f9550874aa3 100644 --- a/Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean +++ b/Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean @@ -3,7 +3,7 @@ Copyright (c) 2023 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic import Mathlib.Dynamics.BirkhoffSum.Average /-! diff --git a/Mathlib/MeasureTheory/Function/L2Space.lean b/Mathlib/MeasureTheory/Function/L2Space.lean index 00991dbbc8dff..9a070391cdaba 100644 --- a/Mathlib/MeasureTheory/Function/L2Space.lean +++ b/Mathlib/MeasureTheory/Function/L2Space.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Rémy Degenne. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne -/ -import Mathlib.Data.RCLike.Lemmas +import Mathlib.Analysis.RCLike.Lemmas import Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner import Mathlib.MeasureTheory.Integral.SetIntegral diff --git a/Mathlib/MeasureTheory/Function/SpecialFunctions/RCLike.lean b/Mathlib/MeasureTheory/Function/SpecialFunctions/RCLike.lean index 2d0332092383d..bc99f9c3b59dd 100644 --- a/Mathlib/MeasureTheory/Function/SpecialFunctions/RCLike.lean +++ b/Mathlib/MeasureTheory/Function/SpecialFunctions/RCLike.lean @@ -3,7 +3,7 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ -import Mathlib.Data.RCLike.Lemmas +import Mathlib.Analysis.RCLike.Lemmas import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex #align_import measure_theory.function.special_functions.is_R_or_C from "leanprover-community/mathlib"@"83a66c8775fa14ee5180c85cab98e970956401ad" diff --git a/Mathlib/NumberTheory/SumPrimeReciprocals.lean b/Mathlib/NumberTheory/SumPrimeReciprocals.lean index 228202c77b127..41e6d91a794b9 100644 --- a/Mathlib/NumberTheory/SumPrimeReciprocals.lean +++ b/Mathlib/NumberTheory/SumPrimeReciprocals.lean @@ -27,7 +27,7 @@ open scoped BigOperators Topology /-- The cardinality of the set of `k`-rough numbers `≤ N` is bounded by `N` times the sum of `1/p` over the primes `k ≤ p ≤ N`. -/ --- This needs `Mathlib.Data.RCLike.Basic`, so we put it here +-- This needs `Mathlib.Analysis.RCLike.Basic`, so we put it here -- instead of in `Mathlib.NumberTheory.SmoothNumbers`. lemma Nat.roughNumbersUpTo_card_le' (N k : ℕ) : (roughNumbersUpTo N k).card ≤ diff --git a/Mathlib/Topology/ContinuousFunction/Ideals.lean b/Mathlib/Topology/ContinuousFunction/Ideals.lean index 8a51339e59061..ddb81bacedcfa 100644 --- a/Mathlib/Topology/ContinuousFunction/Ideals.lean +++ b/Mathlib/Topology/ContinuousFunction/Ideals.lean @@ -6,7 +6,7 @@ Authors: Jireh Loreaux import Mathlib.Topology.Algebra.Algebra import Mathlib.Topology.ContinuousFunction.Compact import Mathlib.Topology.UrysohnsLemma -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic import Mathlib.Analysis.NormedSpace.Units import Mathlib.Topology.Algebra.Module.CharacterSpace diff --git a/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean index b311f3d833e0e..2167de9c57d7e 100644 --- a/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean +++ b/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison, Heather Macbeth -/ -import Mathlib.Data.RCLike.Basic +import Mathlib.Analysis.RCLike.Basic import Mathlib.Topology.Algebra.StarSubalgebra import Mathlib.Topology.ContinuousFunction.Weierstrass