Skip to content

Commit b3e0439

Browse files
peabrainiacReemMelamed
authored andcommitted
chore(Algebra): module deprecations for moved AddTorsor files (leanprover-community#39134)
1 parent cea1c55 commit b3e0439

5 files changed

Lines changed: 24 additions & 0 deletions

File tree

Mathlib.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ public import Std
44
public import Batteries
55
public import Mathlib.Algebra.AddConstMap.Basic
66
public import Mathlib.Algebra.AddConstMap.Equiv
7+
public import Mathlib.Algebra.AddTorsor.Basic
8+
public import Mathlib.Algebra.AddTorsor.Defs
79
public import Mathlib.Algebra.AffineMonoid.Basic
810
public import Mathlib.Algebra.AffineMonoid.Embedding
911
public import Mathlib.Algebra.AffineMonoid.Irreducible
@@ -7499,6 +7501,7 @@ public import Mathlib.Topology.Algebra.ContinuousMonoidHom
74997501
public import Mathlib.Topology.Algebra.Equicontinuity
75007502
public import Mathlib.Topology.Algebra.Field
75017503
public import Mathlib.Topology.Algebra.FilterBasis
7504+
public import Mathlib.Topology.Algebra.Group.AddTorsor
75027505
public import Mathlib.Topology.Algebra.Group.Basic
75037506
public import Mathlib.Topology.Algebra.Group.ClosedSubgroup
75047507
public import Mathlib.Topology.Algebra.Group.Compact
@@ -7613,6 +7616,7 @@ public import Mathlib.Topology.Algebra.Order.Support
76137616
public import Mathlib.Topology.Algebra.Order.UpperLower
76147617
public import Mathlib.Topology.Algebra.Polynomial
76157618
public import Mathlib.Topology.Algebra.PontryaginDual
7619+
public import Mathlib.Topology.Algebra.ProperAction.AddTorsor
76167620
public import Mathlib.Topology.Algebra.ProperAction.Basic
76177621
public import Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
76187622
public import Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous
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.Algebra.Torsor.Basic
4+
5+
deprecated_module (since := "2026-06-12")
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.Algebra.Torsor.Defs
4+
5+
deprecated_module (since := "2026-06-12")
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.Group.Torsor
4+
5+
deprecated_module (since := "2026-06-12")
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.ProperAction.Torsor
4+
5+
deprecated_module (since := "2026-06-12")

0 commit comments

Comments
 (0)