Skip to content

Commit a38ceed

Browse files
committed
chore(NumberField): follow-up to leanprover-community#30536 (leanprover-community#30583)
Create the deprecated module files for the files moved in leanprover-community#30536
1 parent ab46cf6 commit a38ceed

File tree

5 files changed

+16
-0
lines changed

5 files changed

+16
-0
lines changed

Mathlib.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4859,8 +4859,12 @@ import Mathlib.NumberTheory.ClassNumber.FunctionField
48594859
import Mathlib.NumberTheory.Cyclotomic.Basic
48604860
import Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
48614861
import Mathlib.NumberTheory.Cyclotomic.Discriminant
4862+
import Mathlib.NumberTheory.Cyclotomic.Embeddings
48624863
import Mathlib.NumberTheory.Cyclotomic.Gal
4864+
import Mathlib.NumberTheory.Cyclotomic.PID
48634865
import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
4866+
import Mathlib.NumberTheory.Cyclotomic.Rat
4867+
import Mathlib.NumberTheory.Cyclotomic.Three
48644868
import Mathlib.NumberTheory.Dioph
48654869
import Mathlib.NumberTheory.DiophantineApproximation.Basic
48664870
import Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
import Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
2+
3+
deprecated_module (since := "2025-10-14")
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
2+
3+
deprecated_module (since := "2025-10-14")
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
2+
3+
deprecated_module (since := "2025-10-14")
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
import Mathlib.NumberTheory.NumberField.Cyclotomic.Three
2+
3+
deprecated_module (since := "2025-10-14")

0 commit comments

Comments
 (0)