From 6b09cba21b9209638a8c407d282ec3e84e3bebe5 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Thu, 21 May 2026 21:16:46 +0200 Subject: [PATCH 1/3] chore(Topology/Algebra/Module/LinearMap): deprecate_module --- Mathlib.lean | 1 + Mathlib/Topology/Algebra/Module/LinearMap.lean | 9 +++++++++ 2 files changed, 10 insertions(+) create mode 100644 Mathlib/Topology/Algebra/Module/LinearMap.lean diff --git a/Mathlib.lean b/Mathlib.lean index 2e6f05fb7e70c2..2078336488e09f 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7474,6 +7474,7 @@ public import Mathlib.Topology.Algebra.Module.Determinant public import Mathlib.Topology.Algebra.Module.Equiv public import Mathlib.Topology.Algebra.Module.FiniteDimension public import Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear +public import Mathlib.Topology.Algebra.Module.LinearMap public import Mathlib.Topology.Algebra.Module.LinearPMap public import Mathlib.Topology.Algebra.Module.LocallyConvex public import Mathlib.Topology.Algebra.Module.ModuleTopology diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean new file mode 100644 index 00000000000000..9b2c3ac60cfd46 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/LinearMap.lean @@ -0,0 +1,9 @@ +module -- shake: keep-all + +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars + +deprecated_module (since := "2026-05-21") From 23d09c640daca5c8d52686748d5e1810049fdd28 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Thu, 21 May 2026 23:34:27 +0200 Subject: [PATCH 2/3] second deprecation --- Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean diff --git a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean new file mode 100644 index 00000000000000..2028364d8e75ad --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean @@ -0,0 +1,5 @@ +module -- shake: keep-all + +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd + +deprecated_module (since := "2026-05-21") From 50178899074c2d6f7d13ff4a1ed86a521782de5f Mon Sep 17 00:00:00 2001 From: ADedecker Date: Thu, 21 May 2026 23:41:07 +0200 Subject: [PATCH 3/3] mk_all --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 2078336488e09f..788c3262b42970 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7475,6 +7475,7 @@ public import Mathlib.Topology.Algebra.Module.Equiv public import Mathlib.Topology.Algebra.Module.FiniteDimension public import Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.LinearMapPiProd public import Mathlib.Topology.Algebra.Module.LinearPMap public import Mathlib.Topology.Algebra.Module.LocallyConvex public import Mathlib.Topology.Algebra.Module.ModuleTopology