Skip to content

Commit be88371

Browse files
committed
chore: add module deprecations for files moved out of Data (#40256)
Follow-up to #39984 and its dependencies.
1 parent 2c8c18c commit be88371

14 files changed

Lines changed: 78 additions & 0 deletions

File tree

Mathlib.lean

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3860,6 +3860,7 @@ public import Mathlib.Data.Fin.Tuple.Take
38603860
public import Mathlib.Data.Fin.VecNotation
38613861
public import Mathlib.Data.FinEnum
38623862
public import Mathlib.Data.FinEnum.Option
3863+
public import Mathlib.Data.Finite.Card
38633864
public import Mathlib.Data.Finite.Defs
38643865
public import Mathlib.Data.Finite.Perm
38653866
public import Mathlib.Data.Finite.Prod
@@ -3978,6 +3979,7 @@ public import Mathlib.Data.Fintype.Shrink
39783979
public import Mathlib.Data.Fintype.Sigma
39793980
public import Mathlib.Data.Fintype.Sort
39803981
public import Mathlib.Data.Fintype.Sum
3982+
public import Mathlib.Data.Fintype.Units
39813983
public import Mathlib.Data.Fintype.Vector
39823984
public import Mathlib.Data.Fintype.WithTopBot
39833985
public import Mathlib.Data.FunLike.Basic
@@ -4090,14 +4092,19 @@ public import Mathlib.Data.List.TakeWhile
40904092
public import Mathlib.Data.List.ToFinsupp
40914093
public import Mathlib.Data.List.Triplewise
40924094
public import Mathlib.Data.List.Zip
4095+
public import Mathlib.Data.Matrix.Action
40934096
public import Mathlib.Data.Matrix.Auto
40944097
public import Mathlib.Data.Matrix.Basic
40954098
public import Mathlib.Data.Matrix.Basis
4099+
public import Mathlib.Data.Matrix.Bilinear
40964100
public import Mathlib.Data.Matrix.Block
4101+
public import Mathlib.Data.Matrix.Cartan
40974102
public import Mathlib.Data.Matrix.ColumnRowPartitioned
40984103
public import Mathlib.Data.Matrix.Composition
40994104
public import Mathlib.Data.Matrix.DMatrix
41004105
public import Mathlib.Data.Matrix.Diagonal
4106+
public import Mathlib.Data.Matrix.DualNumber
4107+
public import Mathlib.Data.Matrix.Invertible
41014108
public import Mathlib.Data.Matrix.Mul
41024109
public import Mathlib.Data.Matrix.PEquiv
41034110
public import Mathlib.Data.Matrix.Reflection
@@ -4273,6 +4280,7 @@ public import Mathlib.Data.QPF.Multivariate.Constructions.Sigma
42734280
public import Mathlib.Data.QPF.Univariate.Basic
42744281
public import Mathlib.Data.Quot
42754282
public import Mathlib.Data.Rat.BigOperators
4283+
public import Mathlib.Data.Rat.Cardinal
42764284
public import Mathlib.Data.Rat.Cast.CharZero
42774285
public import Mathlib.Data.Rat.Cast.Defs
42784286
public import Mathlib.Data.Rat.Cast.Lemmas
@@ -4285,16 +4293,21 @@ public import Mathlib.Data.Rat.Floor
42854293
public import Mathlib.Data.Rat.Init
42864294
public import Mathlib.Data.Rat.Lemmas
42874295
public import Mathlib.Data.Rat.NatSqrt.Defs
4296+
public import Mathlib.Data.Rat.NatSqrt.Real
42884297
public import Mathlib.Data.Rat.Sqrt
42894298
public import Mathlib.Data.Rat.Star
4299+
public import Mathlib.Data.Real.Archimedean
42904300
public import Mathlib.Data.Real.Basic
42914301
public import Mathlib.Data.Real.CompleteField
42924302
public import Mathlib.Data.Real.ConjExponents
42934303
public import Mathlib.Data.Real.ENatENNReal
42944304
public import Mathlib.Data.Real.Embedding
4305+
public import Mathlib.Data.Real.Hom
42954306
public import Mathlib.Data.Real.Pointwise
42964307
public import Mathlib.Data.Real.Sign
4308+
public import Mathlib.Data.Real.Sqrt
42974309
public import Mathlib.Data.Real.Star
4310+
public import Mathlib.Data.Real.StarOrdered
42984311
public import Mathlib.Data.Rel
42994312
public import Mathlib.Data.Rel.Cover
43004313
public import Mathlib.Data.Rel.Separated

Mathlib/Data/Finite/Card.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.SetTheory.Cardinal.NatCard
4+
5+
deprecated_module (since := "2026-06-05")

Mathlib/Data/Fintype/Units.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Algebra.GroupWithZero.Units.Fintype
4+
5+
deprecated_module (since := "2026-06-05")

Mathlib/Data/Matrix/Action.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.LinearAlgebra.Matrix.Action
4+
5+
deprecated_module (since := "2026-06-05")

Mathlib/Data/Matrix/Bilinear.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.LinearAlgebra.Matrix.Bilinear
4+
5+
deprecated_module (since := "2026-06-05")

Mathlib/Data/Matrix/Cartan.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.LinearAlgebra.Matrix.Cartan
4+
5+
deprecated_module (since := "2026-06-05")
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.LinearAlgebra.Matrix.DualNumber
4+
5+
deprecated_module (since := "2026-06-05")
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.LinearAlgebra.Matrix.Invertible
4+
5+
deprecated_module (since := "2026-06-05")

Mathlib/Data/Rat/Cardinal.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.SetTheory.Cardinal.Rat
4+
5+
deprecated_module (since := "2026-06-05")

Mathlib/Data/Rat/NatSqrt/Real.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Analysis.Rat.NatSqrt.Real
4+
5+
deprecated_module (since := "2026-05-29")

0 commit comments

Comments
 (0)