move(RCLike): Move out of Data (#11753)

`RCLike` is an analytic typeclass, hence should be under `Analysis`
leanprover-community · Mar 29, 2024 · 783b6bc · 783b6bc
1 parent e6b2fea
commit 783b6bc
Show file tree

Hide file tree

Showing 22 changed files with 22 additions and 22 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 → Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Data/RCLike/Basic.lean → Mathlib/Analysis/RCLike/Basic.lean
diff --git a/Mathlib/Data/RCLike/Lemmas.lean → Mathlib/Analysis/RCLike/Lemmas.lean b/Mathlib/Data/RCLike/Lemmas.lean → 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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