[Merged by Bors] - chore: add module deprecations for removed files

Mathlib.lean

@@ -44,6 +44,7 @@ import Mathlib.Algebra.Algebra.TransferInstance
 import Mathlib.Algebra.Algebra.Unitization
 import Mathlib.Algebra.Algebra.ZMod
 import Mathlib.Algebra.AlgebraicCard
+import Mathlib.Algebra.ArithmeticGeometric
 import Mathlib.Algebra.Azumaya.Basic
 import Mathlib.Algebra.Azumaya.Defs
 import Mathlib.Algebra.Azumaya.Matrix
@@ -1710,6 +1711,7 @@ import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.EuclideanDist
 import Mathlib.Analysis.InnerProductSpace.GramMatrix
 import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
+import Mathlib.Analysis.InnerProductSpace.Harmonic.Analytic
 import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
 import Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
 import Mathlib.Analysis.InnerProductSpace.JointEigenspace
@@ -1893,6 +1895,7 @@ import Mathlib.Analysis.NormedSpace.Alternating.Basic
 import Mathlib.Analysis.NormedSpace.Alternating.Curry
 import Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin
 import Mathlib.Analysis.NormedSpace.BallAction
+import Mathlib.Analysis.NormedSpace.ConformalLinearMap
 import Mathlib.Analysis.NormedSpace.Connected
 import Mathlib.Analysis.NormedSpace.DualNumber
 import Mathlib.Analysis.NormedSpace.ENormedSpace
@@ -2129,6 +2132,7 @@ import Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
 import Mathlib.CategoryTheory.Bicategory.Functor.Oplax
 import Mathlib.CategoryTheory.Bicategory.Functor.Prelax
 import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
+import Mathlib.CategoryTheory.Bicategory.Functor.Strict
 import Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
 import Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
 import Mathlib.CategoryTheory.Bicategory.Grothendieck
@@ -2142,6 +2146,7 @@ import Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
 import Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
 import Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Strong
 import Mathlib.CategoryTheory.Bicategory.SingleObj
+import Mathlib.CategoryTheory.Bicategory.Strict
 import Mathlib.CategoryTheory.Bicategory.Strict.Basic
 import Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
 import Mathlib.CategoryTheory.CatCommSq
@@ -3550,6 +3555,7 @@ import Mathlib.Data.Nat.PSub
 import Mathlib.Data.Nat.Pairing
 import Mathlib.Data.Nat.PartENat
 import Mathlib.Data.Nat.Periodic
+import Mathlib.Data.Nat.PowModTotient
 import Mathlib.Data.Nat.Prime.Basic
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.Nat.Prime.Factorial
@@ -3639,6 +3645,7 @@ import Mathlib.Data.Real.EReal
 import Mathlib.Data.Real.Embedding
 import Mathlib.Data.Real.GoldenRatio
 import Mathlib.Data.Real.Hyperreal
+import Mathlib.Data.Real.Irrational
 import Mathlib.Data.Real.Pi.Bounds
 import Mathlib.Data.Real.Pi.Irrational
 import Mathlib.Data.Real.Pi.Leibniz
@@ -4165,6 +4172,7 @@ import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
 import Mathlib.LinearAlgebra.AffineSpace.Basis
 import Mathlib.LinearAlgebra.AffineSpace.Centroid
 import Mathlib.LinearAlgebra.AffineSpace.Combination
+import Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv
 import Mathlib.LinearAlgebra.AffineSpace.Defs
 import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import Mathlib.LinearAlgebra.AffineSpace.Independent
@@ -5384,6 +5392,7 @@ import Mathlib.Probability.Martingale.Upcrossing
 import Mathlib.Probability.Moments.Basic
 import Mathlib.Probability.Moments.ComplexMGF
 import Mathlib.Probability.Moments.Covariance
+import Mathlib.Probability.Moments.CovarianceBilin
 import Mathlib.Probability.Moments.CovarianceBilinDual
 import Mathlib.Probability.Moments.IntegrableExpMul
 import Mathlib.Probability.Moments.MGFAnalytic

Mathlib/Algebra/ArithmeticGeometric.lean

@@ -0,0 +1,3 @@
+import Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
+
+deprecated_module (since := "2025-09-17")

Mathlib/Analysis/InnerProductSpace/Harmonic/Analytic.lean

@@ -0,0 +1,3 @@
+import Mathlib.Analysis.Complex.Harmonic.Analytic
+
+deprecated_module (since := "2025-09-16")

Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean

@@ -0,0 +1,3 @@
+import Mathlib.Analysis.Normed.Operator.Conformal
+
+deprecated_module (since := "2025-09-16")

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

@@ -0,0 +1,3 @@
+import Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
+
+deprecated_module (since := "2025-10-02")

Mathlib/CategoryTheory/Bicategory/Strict.lean

@@ -0,0 +1,3 @@
+import Mathlib.CategoryTheory.Bicategory.Strict.Basic
+
+deprecated_module (since := "2025-10-02")

Mathlib/Data/Nat/PowModTotient.lean

@@ -0,0 +1,3 @@
+import Mathlib.NumberTheory.PowModTotient
+
+deprecated_module (since := "2025-09-19")

Mathlib/Data/Real/Irrational.lean

@@ -0,0 +1,3 @@
+import Mathlib.RingTheory.Real.Irrational
+
+deprecated_module (since := "2025-10-13")

Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

@@ -0,0 +1,3 @@
+import Mathlib.Topology.Algebra.ContinuousAffineEquiv
+
+deprecated_module (since := "2025-09-20")

Mathlib/Probability/Moments/CovarianceBilin.lean

@@ -0,0 +1,3 @@
+import Mathlib.Probability.Moments.CovarianceBilinDual
+
+deprecated_module (since := "2025-10-13")