Skip to content

Commit 7ca1685

Browse files
committed
chore(Adjoin/Polynomial): deprecate module (leanprover-community#35913)
Add deprecated module following leanprover-community#35883. Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>
1 parent ce269e5 commit 7ca1685

2 files changed

Lines changed: 6 additions & 0 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6024,6 +6024,7 @@ public import Mathlib.RingTheory.Adjoin.Dimension
60246024
public import Mathlib.RingTheory.Adjoin.FG
60256025
public import Mathlib.RingTheory.Adjoin.FGBaseChange
60266026
public import Mathlib.RingTheory.Adjoin.Field
6027+
public import Mathlib.RingTheory.Adjoin.Polynomial
60276028
public import Mathlib.RingTheory.Adjoin.Polynomial.Basic
60286029
public import Mathlib.RingTheory.Adjoin.PowerBasis
60296030
public import Mathlib.RingTheory.Adjoin.Singleton
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.RingTheory.Adjoin.Polynomial.Basic
4+
5+
deprecated_module (since := "2026-03-01")

0 commit comments

Comments
 (0)