Skip to content

Commit e4037a3

Browse files
committed
chore: Split HahnSeries file (#10595)
The HahnSeries file is approaching 2000 lines, and I was hoping to add some more material on Hahn series in the near future. This PR splits the material roughly according to what structure we see in the coefficients: `Basic` assumes that the coefficient type `R` has zero, `Addition` assumes addition, `Multiplication` more or less assumes some multiplicative structure.
1 parent 9e1a0e7 commit e4037a3

File tree

8 files changed

+2108
-1935
lines changed

8 files changed

+2108
-1935
lines changed

Mathlib.lean

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3211,7 +3211,11 @@ import Mathlib.RingTheory.GradedAlgebra.Basic
32113211
import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
32123212
import Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
32133213
import Mathlib.RingTheory.GradedAlgebra.Radical
3214-
import Mathlib.RingTheory.HahnSeries
3214+
import Mathlib.RingTheory.HahnSeries.Addition
3215+
import Mathlib.RingTheory.HahnSeries.Basic
3216+
import Mathlib.RingTheory.HahnSeries.Multiplication
3217+
import Mathlib.RingTheory.HahnSeries.PowerSeries
3218+
import Mathlib.RingTheory.HahnSeries.Summable
32153219
import Mathlib.RingTheory.Henselian
32163220
import Mathlib.RingTheory.Ideal.AssociatedPrime
32173221
import Mathlib.RingTheory.Ideal.Basic

0 commit comments

Comments
 (0)