Reduced Hahn series

LM24, Definition 8.2.6 calls a nonzero series reduced when the intersection of its support with the support after subtracting one lies in a single Archimedean class. We retain the zero class: ArchimedeanClass.mk 0 = ⊤. This matters when the constant coefficient is neither zero nor one, and distinguishes the printed definition from the incorrect variant that inspects only nonzero exponents.

def HahnSeries.Nonpositive.IsReduced {G : Type u_1} {R : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Ring R] (b : Nonpositive G R) : Prop

LM24, Definition 8.2.6: a nonzero nonpositive Hahn series whose support and shifted support intersect in one Archimedean class. The class may be the zero class ⊤.

Equations

• b.IsReduced = (b ≠ 0 ∧ ∃ (c : ArchimedeanClass G), (↑b).support ∩ (↑(b - 1)).support ⊆ {x : G | ArchimedeanClass.mk x = c})

theorem HahnSeries.Nonpositive.IsReduced.elim {G : Type u_1} {R : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Ring R] {b : Nonpositive G R} (hb : b.IsReduced) : b ≠ 0 ∧ ∃ (c : ArchimedeanClass G), (↑b).support ∩ (↑(b - 1)).support ⊆ {x : G | ArchimedeanClass.mk x = c}

Elimination rule for reducedness.

theorem HahnSeries.Nonpositive.isReduced_of_support_inter_support_sub_one_subset {G : Type u_1} {R : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Ring R] {b : Nonpositive G R} (hb : b ≠ 0) (c : ArchimedeanClass G) (hsupport : (↑b).support ∩ (↑(b - 1)).support ⊆ {x : G | ArchimedeanClass.mk x = c}) : b.IsReduced

Introduction rule for reducedness.