chore: deprecating module LinearAlgebra.PiTensorProduct (#26987)

joelriou · joelriou · commit 609d880957e9 · 2026-06-25T08:42:39.000Z
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -5154,6 +5154,7 @@ public import Mathlib.LinearAlgebra.PID
 public import Mathlib.LinearAlgebra.PerfectPairing.Basic
 public import Mathlib.LinearAlgebra.PerfectPairing.Restrict
 public import Mathlib.LinearAlgebra.Pi
+public import Mathlib.LinearAlgebra.PiTensorProduct
 public import Mathlib.LinearAlgebra.PiTensorProduct.Basic
 public import Mathlib.LinearAlgebra.PiTensorProduct.Basis
 public import Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean
@@ -0,0 +1,5 @@
+module
+
+public import Mathlib.LinearAlgebra.PiTensorProduct.Basic
+
+deprecated_module (since := "2026-06-18")

-Original file line number
+Diff line change
@@ @@ -0,0 +1,5 @@ @@
 +module
++
 +public import Mathlib.LinearAlgebra.PiTensorProduct.Basic
++
 +deprecated_module (since := "2026-06-18")