Skip to content

Commit ff5f36d

Browse files
ADedeckerBergschaf
authored andcommitted
chore(Topology/Algebra/Module/LinearMap): deprecate_module (leanprover-community#39668)
Also covers the `.../LinearMapPiProd.lean` -> `.../ContinuousLinearMap/PiProd.lean` move. Follow-up for leanprover-community#39612
1 parent a62542b commit ff5f36d

3 files changed

Lines changed: 16 additions & 0 deletions

File tree

Mathlib.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7474,6 +7474,8 @@ public import Mathlib.Topology.Algebra.Module.Determinant
74747474
public import Mathlib.Topology.Algebra.Module.Equiv
74757475
public import Mathlib.Topology.Algebra.Module.FiniteDimension
74767476
public import Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
7477+
public import Mathlib.Topology.Algebra.Module.LinearMap
7478+
public import Mathlib.Topology.Algebra.Module.LinearMapPiProd
74777479
public import Mathlib.Topology.Algebra.Module.LinearPMap
74787480
public import Mathlib.Topology.Algebra.Module.LocallyConvex
74797481
public import Mathlib.Topology.Algebra.Module.ModuleTopology
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module -- shake: keep-all
2+
3+
public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
4+
public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
5+
public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
6+
public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
7+
public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
8+
9+
deprecated_module (since := "2026-05-21")
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module -- shake: keep-all
2+
3+
public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
4+
5+
deprecated_module (since := "2026-05-21")

0 commit comments

Comments
 (0)