Multiplicative properties of Hahn series

If Γ is ordered and R has zero, then R⟦Γ⟧ consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered. This module introduces multiplication and scalar multiplication on Hahn series. If Γ is an ordered cancellative commutative additive monoid and R is a semiring, then we get a semiring structure on R⟦Γ⟧. If Γ has an ordered vector-addition on Γ' and R has a scalar multiplication on V, we define HahnModule Γ' R V as a type alias for V⟦Γ'⟧ that admits a scalar multiplication from R⟦Γ⟧. The scalar action of R on R⟦Γ⟧ is compatible with the action of R⟦Γ⟧ on HahnModule Γ' R V.

Main Definitions

• HahnModule is a type alias for HahnSeries, which we use for defining scalar multiplication of R⟦Γ⟧ on HahnModule Γ' R V for an R-module V, where Γ' admits an ordered cancellative vector addition operation from Γ. The type alias allows us to avoid a potential instance diamond.
• HahnModule.of is the isomorphism from V⟦Γ⟧ to HahnModule Γ R V.
• HahnSeries.C is the constant term ring homomorphism R →+* R⟦Γ⟧.
• HahnSeries.embDomainRingHom is the ring homomorphism R⟦Γ⟧ →+* R⟦Γ'⟧ induced by an order embedding Γ ↪o Γ'.
• HahnSeries.orderTopSubOnePos is the group of invertible Hahn series close to 1, i.e., those series such that subtracting one yields a series with strictly positive orderTop.

Main results

• If R is a (commutative) (semi-)ring, then so is R⟦Γ⟧.
• If V is an R-module, then HahnModule Γ' R V is a R⟦Γ⟧-module.

TODO

The following may be useful for composing vertex operators, but they seem to take time.

• rightTensorMap: HahnModule Γ' R U ⊗[R] V →ₗ[R] HahnModule Γ' R (U ⊗[R] V)
• leftTensorMap: U ⊗[R] HahnModule Γ' R V →ₗ[R] HahnModule Γ' R (U ⊗[R] V)

References

• [J. van der Hoeven, Operators on Generalized Power Series][van_der_hoeven]

instance HahnSeries.instOne {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [One R] : One (HahnSeries Γ R)

instance HahnSeries.instNatCast {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [NatCast R] : NatCast (HahnSeries Γ R)

instance HahnSeries.instIntCast {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [IntCast R] : IntCast (HahnSeries Γ R)

instance HahnSeries.instNNRatCast {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [NNRatCast R] : NNRatCast (HahnSeries Γ R)

instance HahnSeries.instRatCast {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [RatCast R] : RatCast (HahnSeries Γ R)

@[simp]

theorem HahnSeries.coeff_one {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [One R] {a : Γ} : coeff 1 a = if a = 0 then 1 else 0

@[simp]

theorem HahnSeries.single_zero_one {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [One R] : (single 0) 1 = 1

theorem HahnSeries.single_zero_natCast {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [NatCast R] (n : ℕ) : (single 0) ↑n = ↑n

theorem HahnSeries.single_zero_intCast {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [IntCast R] (z : ℤ) : (single 0) ↑z = ↑z

theorem HahnSeries.single_zero_nnratCast {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [NNRatCast R] (q : ℚ≥0) : (single 0) ↑q = ↑q

theorem HahnSeries.single_zero_ratCast {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [RatCast R] (q : ℚ) : (single 0) ↑q = ↑q

theorem HahnSeries.single_zero_ofNat {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [NatCast R] (n : ℕ) [n.AtLeastTwo] : (single 0) (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem HahnSeries.support_one {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [MulZeroOneClass R] [Nontrivial R] : support 1 = {0}

@[simp]

theorem HahnSeries.orderTop_one {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [Zero R] [One R] [NeZero 1] : orderTop 1 = 0

@[simp]

theorem HahnSeries.order_one {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [MulZeroOneClass R] : order 1 = 0

@[simp]

theorem HahnSeries.leadingCoeff_one {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [MulZeroOneClass R] : leadingCoeff 1 = 1

@[simp]

theorem HahnSeries.map_one {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [Zero Γ] [PartialOrder Γ] [MonoidWithZero R] [MonoidWithZero S] (f : R →*₀ S) : map 1 f = 1

instance HahnSeries.instAddCommMonoidWithOne {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [AddCommMonoidWithOne R] : AddCommMonoidWithOne (HahnSeries Γ R)

instance HahnSeries.instAddCommGroupWithOne {Γ : Type u_1} {R : Type u_3} [Zero Γ] [PartialOrder Γ] [AddCommGroupWithOne R] : AddCommGroupWithOne (HahnSeries Γ R)

def HahnModule (Γ : Type u_6) (R : Type u_7) (V : Type u_8) [PartialOrder Γ] [Zero V] [SMul R V] : Type (max u_6 u_8)

We introduce a type alias for HahnSeries in order to work with scalar multiplication by series. If we wrote a SMul R⟦Γ⟧ V⟦Γ⟧ instance, then when V = R⟦Γ⟧, we would have two different actions of R⟦Γ⟧ on V⟦Γ⟧. See Mathlib/Algebra/Polynomial/Module/Basic.lean for more discussion on this problem.

def HahnModule.of {Γ : Type u_1} {V : Type u_5} [PartialOrder Γ] [Zero V] (R : Type u_6) [SMul R V] : HahnSeries Γ V ≃ HahnModule Γ R V

The casting function to the type synonym.

def HahnModule.rec {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [Zero V] [SMul R V] {motive : HahnModule Γ R V → Sort u_6} (h : (x : HahnSeries Γ V) → motive ((of R) x)) (x : HahnModule Γ R V) : motive x

Recursion principle to reduce a result about the synonym to the original type.

theorem HahnModule.ext {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [Zero V] [SMul R V] (x y : HahnModule Γ R V) (h : ((of R).symm x).coeff = ((of R).symm y).coeff) : x = y

theorem HahnModule.ext_iff {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [Zero V] [SMul R V] {x y : HahnModule Γ R V} : x = y ↔ ((of R).symm x).coeff = ((of R).symm y).coeff

instance HahnModule.instZero {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [Zero V] : Zero (HahnModule Γ R V)

instance HahnModule.instAddCommMonoid {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [AddCommMonoid V] : AddCommMonoid (HahnModule Γ R V)

instance HahnModule.instAddCommGroup {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [AddCommGroup V] : AddCommGroup (HahnModule Γ R V)

instance HahnModule.instBaseSMul {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_6} [Monoid R] [AddMonoid V] [DistribMulAction R V] : SMul R (HahnModule Γ R V)

@[simp]

theorem HahnModule.of_zero {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [Zero V] : (of R) 0 = 0

@[simp]

theorem HahnModule.of_add {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [AddCommMonoid V] (x y : HahnSeries Γ V) : (of R) (x + y) = (of R) x + (of R) y

@[simp]

theorem HahnModule.of_sub {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [AddCommGroup V] (x y : HahnSeries Γ V) : (of R) (x - y) = (of R) x - (of R) y

@[simp]

theorem HahnModule.of_symm_zero {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [Zero V] : (of R).symm 0 = 0

@[simp]

theorem HahnModule.of_symm_add {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [AddCommMonoid V] (x y : HahnModule Γ R V) : (of R).symm (x + y) = (of R).symm x + (of R).symm y

@[simp]

theorem HahnModule.of_symm_sub {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [AddCommGroup V] (x y : HahnModule Γ R V) : (of R).symm (x - y) = (of R).symm x - (of R).symm y

instance HahnModule.instSMul {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [Zero R] [AddCommMonoid V] : SMul (HahnSeries Γ R) (HahnModule Γ' R V)

theorem HahnModule.coeff_smul {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [SMul R V] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [Zero R] [AddCommMonoid V] (x : HahnSeries Γ R) (y : HahnModule Γ' R V) (a : Γ') : ((of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal ⋯ ⋯ a, x.coeff ij.1 • ((of R).symm y).coeff ij.2

instance HahnModule.instBaseSMulZeroClass {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [AddCommMonoid V] [SMulZeroClass R V] : SMulZeroClass R (HahnModule Γ R V)

@[simp]

theorem HahnModule.of_smul {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [AddCommMonoid V] [SMulZeroClass R V] (r : R) (x : HahnSeries Γ V) : (of R) (r • x) = r • (of R) x

@[simp]

theorem HahnModule.of_symm_smul {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [AddCommMonoid V] [SMulZeroClass R V] (r : R) (x : HahnModule Γ R V) : (of R).symm (r • x) = r • (of R).symm x

instance HahnModule.instSMulZeroClass {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Zero R] [SMulZeroClass R V] : SMulZeroClass (HahnSeries Γ R) (HahnModule Γ' R V)

theorem HahnModule.coeff_smul_right {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Zero R] [SMulZeroClass R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ'} (hs : s.IsPWO) (hys : ((of R).symm y).support ⊆ s) : ((of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((of R).symm y).coeff ij.2

theorem HahnModule.coeff_smul_left {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Zero R] [SMulWithZero R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ} (hs : s.IsPWO) (hxs : x.support ⊆ s) : ((of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal hs ⋯ a, x.coeff ij.1 • ((of R).symm y).coeff ij.2

theorem HahnModule.smul_add {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Zero R] [DistribSMul R V] (x : HahnSeries Γ R) (y z : HahnModule Γ' R V) : x • (y + z) = x • y + x • z

instance HahnModule.instDistribSMul {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [MonoidWithZero R] [DistribSMul R V] : DistribSMul (HahnSeries Γ R) (HahnModule Γ' R V)

theorem HahnModule.add_smul {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] {x y : HahnSeries Γ R} {z : HahnModule Γ' R V} (h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u) : (x + y) • z = x • z + y • z

theorem HahnModule.coeff_single_smul_vadd {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [MulZeroClass R] [SMulWithZero R V] {r : R} {x : HahnModule Γ' R V} {a : Γ'} {b : Γ} : ((of R).symm ((HahnSeries.single b) r • x)).coeff (b +ᵥ a) = r • ((of R).symm x).coeff a

theorem HahnModule.coeff_single_zero_smul {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ'] [AddCommMonoid V] {Γ : Type u_6} [AddCommMonoid Γ] [PartialOrder Γ] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [MulZeroClass R] [SMulWithZero R V] {r : R} {x : HahnModule Γ' R V} {a : Γ'} : ((of R).symm ((HahnSeries.single 0) r • x)).coeff a = r • ((of R).symm x).coeff a

@[simp]

theorem HahnModule.single_zero_smul_eq_smul {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ'] [AddCommMonoid V] (Γ : Type u_6) [AddCommMonoid Γ] [PartialOrder Γ] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [MulZeroClass R] [SMulWithZero R V] {r : R} {x : HahnModule Γ' R V} : (HahnSeries.single 0) r • x = r • x

@[simp]

theorem HahnModule.zero_smul' {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Zero R] [SMulWithZero R V] {x : HahnModule Γ' R V} : 0 • x = 0

@[simp]

theorem HahnModule.one_smul' {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ'] [AddCommMonoid V] {Γ : Type u_6} [AddCommMonoid Γ] [PartialOrder Γ] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [MonoidWithZero R] [MulActionWithZero R V] {x : HahnModule Γ' R V} : 1 • x = x

theorem HahnModule.support_smul_subset_vadd_support' {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [MulZeroClass R] [SMulWithZero R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} : ((of R).symm (x • y)).support ⊆ x.support +ᵥ ((of R).symm y).support

theorem HahnModule.support_smul_subset_vadd_support {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [MulZeroClass R] [SMulWithZero R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} : ((of R).symm (x • y)).support ⊆ x.support +ᵥ ((of R).symm y).support

theorem HahnModule.orderTop_vAdd_le_orderTop_smul {R : Type u_3} {V : Type u_5} [AddCommMonoid V] {Γ : Type u_6} {Γ' : Type u_7} [LinearOrder Γ] [LinearOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [MulZeroClass R] [SMulWithZero R V] {x : HahnSeries Γ R} [VAdd (WithTop Γ) (WithTop Γ')] {y : HahnModule Γ' R V} (h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ') : x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

theorem HahnModule.coeff_smul_order_add_order {R : Type u_3} {V : Type u_5} [AddCommMonoid V] {Γ : Type u_6} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Zero R] [SMulWithZero R V] (x : HahnSeries Γ R) (y : HahnModule Γ R V) : ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

instance HahnSeries.instMul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] : Mul (HahnSeries Γ R)

theorem HahnSeries.of_symm_smul_of_eq_mul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} : (HahnModule.of R).symm (x • (HahnModule.of R) y) = x * y

theorem HahnSeries.coeff_mul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} : (x * y).coeff a = ∑ ij ∈ Finset.addAntidiagonal ⋯ ⋯ a, x.coeff ij.1 * y.coeff ij.2

theorem HahnSeries.map_mul {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) {x y : HahnSeries Γ R} : (x * y).map f = x.map f * y.map f

theorem HahnSeries.coeff_mul_left' {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} {s : Set Γ} (hs : s.IsPWO) (hxs : x.support ⊆ s) : (x * y).coeff a = ∑ ij ∈ Finset.addAntidiagonal hs ⋯ a, x.coeff ij.1 * y.coeff ij.2

theorem HahnSeries.coeff_mul_right' {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} {s : Set Γ} (hs : s.IsPWO) (hys : y.support ⊆ s) : (x * y).coeff a = ∑ ij ∈ Finset.addAntidiagonal ⋯ hs a, x.coeff ij.1 * y.coeff ij.2

instance HahnSeries.instDistrib {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] : Distrib (HahnSeries Γ R)

theorem HahnSeries.coeff_single_mul_add {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a b : Γ} : ((single b) r * x).coeff (a + b) = r * x.coeff a

theorem HahnSeries.coeff_mul_single_add {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a b : Γ} : (x * (single b) r).coeff (a + b) = x.coeff a * r

theorem HahnSeries.coeff_single_mul {Γ' : Type u_2} {R : Type u_3} [NonUnitalNonAssocSemiring R] [PartialOrder Γ'] [AddCommGroup Γ'] [IsOrderedAddMonoid Γ'] {r : R} {x : HahnSeries Γ' R} {a b : Γ'} : ((single b) r * x).coeff a = r * x.coeff (a - b)

theorem HahnSeries.coeff_mul_single {Γ' : Type u_2} {R : Type u_3} [NonUnitalNonAssocSemiring R] [PartialOrder Γ'] [AddCommGroup Γ'] [IsOrderedAddMonoid Γ'] {r : R} {x : HahnSeries Γ' R} {a b : Γ'} : (x * (single b) r).coeff a = x.coeff (a - b) * r

@[simp]

theorem HahnSeries.coeff_mul_single_zero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} : (x * (single 0) r).coeff a = x.coeff a * r

theorem HahnSeries.coeff_single_zero_mul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} : ((single 0) r * x).coeff a = r * x.coeff a

@[simp]

theorem HahnSeries.single_zero_mul_eq_smul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {r : R} {x : HahnSeries Γ R} : (single 0) r * x = r • x

theorem HahnSeries.support_mul_subset {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} : (x * y).support ⊆ x.support + y.support

@[deprecated HahnSeries.support_mul_subset (since := "2025-12-09")]

theorem HahnSeries.support_mul_subset_add_support {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} : (x * y).support ⊆ x.support + y.support

Alias of HahnSeries.support_mul_subset.

instance HahnSeries.instNonUnitalNonAssocSemiring {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (HahnSeries Γ R)

theorem HahnSeries.coeff_mul_order_add_order {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] (x y : HahnSeries Γ R) : (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

theorem HahnSeries.orderTop_mul_of_ne_zero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} (h : x.leadingCoeff * y.leadingCoeff ≠ 0) : (x * y).orderTop = x.orderTop + y.orderTop

@[deprecated HahnSeries.orderTop_mul_of_ne_zero (since := "2026-01-02")]

theorem HahnSeries.orderTop_mul_of_nonzero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} (h : x.leadingCoeff * y.leadingCoeff ≠ 0) : (x * y).orderTop = x.orderTop + y.orderTop

Alias of HahnSeries.orderTop_mul_of_ne_zero.

@[simp]

theorem HahnSeries.orderTop_mul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] (x y : HahnSeries Γ R) [NoZeroDivisors R] : (x * y).orderTop = x.orderTop + y.orderTop

theorem HahnSeries.orderTop_add_le_mul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} : x.orderTop + y.orderTop ≤ (x * y).orderTop

theorem HahnSeries.order_mul_of_ne_zero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} (h : x.leadingCoeff * y.leadingCoeff ≠ 0) : (x * y).order = x.order + y.order

@[deprecated HahnSeries.order_mul_of_ne_zero (since := "2026-01-02")]

theorem HahnSeries.order_mul_of_nonzero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} (h : x.leadingCoeff * y.leadingCoeff ≠ 0) : (x * y).order = x.order + y.order

Alias of HahnSeries.order_mul_of_ne_zero.

theorem HahnSeries.leadingCoeff_mul_of_ne_zero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} (h : x.leadingCoeff * y.leadingCoeff ≠ 0) : (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

@[deprecated HahnSeries.leadingCoeff_mul_of_ne_zero (since := "2026-01-02")]

theorem HahnSeries.leadingCoeff_mul_of_nonzero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} (h : x.leadingCoeff * y.leadingCoeff ≠ 0) : (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Alias of HahnSeries.leadingCoeff_mul_of_ne_zero.

@[simp]

theorem HahnSeries.leadingCoeff_mul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] (x y : HahnSeries Γ R) [NoZeroDivisors R] : (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

theorem HahnSeries.order_single_mul_of_isRegular {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {g : Γ} {r : R} (hr : IsRegular r) {x : HahnSeries Γ R} (hx : x ≠ 0) : ((single g) r * x).order = g + x.order

instance HahnSeries.instNonUnitalSemiring {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalSemiring R] : NonUnitalSemiring (HahnSeries Γ R)

instance HahnSeries.instNonAssocSemiring {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] : NonAssocSemiring (HahnSeries Γ R)

instance HahnSeries.instSemiring {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] : Semiring (HahnSeries Γ R)

instance HahnSeries.instNonUnitalCommSemiring {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalCommSemiring R] : NonUnitalCommSemiring (HahnSeries Γ R)

instance HahnSeries.instCommSemiring {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] : CommSemiring (HahnSeries Γ R)

instance HahnSeries.instNonUnitalNonAssocRing {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (HahnSeries Γ R)

instance HahnSeries.instNonUnitalRing {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalRing R] : NonUnitalRing (HahnSeries Γ R)

instance HahnSeries.instNonAssocRing {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocRing R] : NonAssocRing (HahnSeries Γ R)

instance HahnSeries.instRing {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] : Ring (HahnSeries Γ R)

instance HahnSeries.instNonUnitalCommRing {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalCommRing R] : NonUnitalCommRing (HahnSeries Γ R)

instance HahnSeries.instCommRing {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] : CommRing (HahnSeries Γ R)

theorem HahnSeries.orderTop_nsmul_le_orderTop_pow {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {x : HahnSeries Γ R} {n : ℕ} : n • x.orderTop ≤ (x ^ n).orderTop

theorem HahnSeries.orderTop_self_sub_one_pos_iff {Γ : Type u_1} {R : Type u_3} [LinearOrder Γ] [Zero Γ] [NonAssocRing R] [Nontrivial R] (x : HahnSeries Γ R) : 0 < (x - 1).orderTop ↔ x.orderTop = 0 ∧ x.leadingCoeff = 1

theorem HahnSeries.orderTop_sub_pos {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero Γ] [AddCommGroup R] [One R] {g : Γ} (hg : 0 < g) (r : R) : 0 < (1 + (single g) r - 1).orderTop

def HahnSeries.orderTopSubOnePos (Γ : Type u_6) (R : Type u_7) [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] : Subgroup (HahnSeries Γ R)ˣ

The group of invertible Hahn series close to 1, i.e., those series such that subtracting 1 yields a series with strictly positive orderTop.

@[simp]

theorem HahnSeries.mem_orderTopSubOnePos_iff {Γ : Type u_1} {R : Type u_3} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : (HahnSeries Γ R)ˣ) : x ∈ orderTopSubOnePos Γ R ↔ 0 < (↑x - 1).orderTop

instance HahnModule.instBaseModule {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ'] [AddCommMonoid V] [Semiring R] [Module R V] : Module R (HahnModule Γ' R V)

instance HahnModule.instModule {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [PartialOrder Γ'] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Semiring R] [Module R V] : Module (HahnSeries Γ R) (HahnModule Γ' R V)

instance HahnModule.instIsScalarTowerHahnSeries {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [AddCommMonoid V] [Zero R] {S : Type u_6} [Zero S] [SMul R S] [SMulWithZero R V] [SMulWithZero S V] [IsScalarTower R S V] : IsScalarTower R S (HahnSeries Γ V)

instance HahnModule.instIsScalarTowerHahnSeries_1 {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [PartialOrder Γ'] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Semiring R] [Module R V] : IsScalarTower R (HahnSeries Γ R) (HahnModule Γ' R V)

instance HahnModule.SMulCommClass {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [PartialOrder Γ'] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [CommSemiring R] [Module R V] : _root_.SMulCommClass R (HahnSeries Γ R) (HahnModule Γ' R V)

instance HahnModule.instIsTorsionFree {R : Type u_3} {Γ : Type u_6} {V : Type u_7} [Ring R] [IsDomain R] [AddCommGroup V] [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Module R V] [Module.IsTorsionFree R V] : Module.IsTorsionFree (HahnSeries Γ R) (HahnModule Γ R V)

@[simp]

theorem HahnSeries.single_mul_single {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] {a b : Γ} {r s : R} : (single a) r * (single b) s = (single (a + b)) (r * s)

@[simp]

theorem HahnSeries.single_pow {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (a : Γ) (n : ℕ) (r : R) : (single a) r ^ n = (single (n • a)) (r ^ n)

def HahnSeries.C {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] : R →+* HahnSeries Γ R

C a is the constant Hahn Series a. C is provided as a ring homomorphism.

@[simp]

theorem HahnSeries.C_apply {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] (a : R) : C a = (single 0) a

theorem HahnSeries.C_zero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] : C 0 = 0

theorem HahnSeries.C_one {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] : C 1 = 1

theorem HahnSeries.map_C {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] [NonAssocSemiring S] (a : R) (f : R →+* S) : (C a).map f = C (f a)

theorem HahnSeries.C_injective {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] : Function.Injective ⇑C

theorem HahnSeries.C_ne_zero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] {r : R} (h : r ≠ 0) : C r ≠ 0

theorem HahnSeries.order_C {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] {r : R} : (C r).order = 0

theorem HahnSeries.C_mul_eq_smul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {r : R} {x : HahnSeries Γ R} : C r * x = r • x

theorem HahnSeries.embDomain_mul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] {Γ' : Type u_6} [AddCommMonoid Γ'] [PartialOrder Γ'] [IsOrderedCancelAddMonoid Γ'] [NonUnitalNonAssocSemiring R] (f : Γ ↪o Γ') (hf : ∀ (x y : Γ), f (x + y) = f x + f y) (x y : HahnSeries Γ R) : embDomain f (x * y) = embDomain f x * embDomain f y

theorem HahnSeries.embDomain_one {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] {Γ' : Type u_6} [AddCommMonoid Γ'] [PartialOrder Γ'] [NonAssocSemiring R] (f : Γ ↪o Γ') (hf : f 0 = 0) : embDomain f 1 = 1

def HahnSeries.embDomainRingHom {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] {Γ' : Type u_6} [AddCommMonoid Γ'] [PartialOrder Γ'] [IsOrderedCancelAddMonoid Γ'] [NonAssocSemiring R] (f : Γ →+ Γ') (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') : HahnSeries Γ R →+* HahnSeries Γ' R

Extending the domain of Hahn series is a ring homomorphism.

@[simp]

theorem HahnSeries.embDomainRingHom_apply {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] {Γ' : Type u_6} [AddCommMonoid Γ'] [PartialOrder Γ'] [IsOrderedCancelAddMonoid Γ'] [NonAssocSemiring R] (f : Γ →+ Γ') (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') (a✝ : HahnSeries Γ R) : (embDomainRingHom f hfi hf) a✝ = embDomain { toFun := ⇑f, inj' := hfi, map_rel_iff' := ⋯ } a✝

theorem HahnSeries.embDomainRingHom_C {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] {Γ' : Type u_6} [AddCommMonoid Γ'] [PartialOrder Γ'] [IsOrderedCancelAddMonoid Γ'] [NonAssocSemiring R] {f : Γ →+ Γ'} {hfi : Function.Injective ⇑f} {hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'} {r : R} : (embDomainRingHom f hfi hf) (C r) = C r

instance HahnSeries.instAlgebra {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] {A : Type u_6} [Semiring A] [Algebra R A] : Algebra R (HahnSeries Γ A)

theorem HahnSeries.C_eq_algebraMap {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] : C = algebraMap R (HahnSeries Γ R)

theorem HahnSeries.algebraMap_apply {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] {A : Type u_6} [Semiring A] [Algebra R A] {r : R} : (algebraMap R (HahnSeries Γ A)) r = C ((algebraMap R A) r)

instance HahnSeries.instNontrivialSubalgebra {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [Nontrivial Γ] [Nontrivial R] : Nontrivial (Subalgebra R (HahnSeries Γ R))

def HahnSeries.embDomainAlgHom {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] {A : Type u_6} [Semiring A] [Algebra R A] {Γ' : Type u_7} [AddCommMonoid Γ'] [PartialOrder Γ'] [IsOrderedCancelAddMonoid Γ'] (f : Γ →+ Γ') (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') : HahnSeries Γ A →ₐ[R] HahnSeries Γ' A

Extending the domain of Hahn series is an algebra homomorphism.

@[simp]

theorem HahnSeries.embDomainAlgHom_apply_coeff {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] {A : Type u_6} [Semiring A] [Algebra R A] {Γ' : Type u_7} [AddCommMonoid Γ'] [PartialOrder Γ'] [IsOrderedCancelAddMonoid Γ'] (f : Γ →+ Γ') (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') (a✝ : HahnSeries Γ A) (b : Γ') : ((embDomainAlgHom f hfi hf) a✝).coeff b = if h : b ∈ ⇑f '' a✝.support then a✝.coeff (Classical.choose ⋯) else 0

instance HahnSeries.instIsCancelMulZeroOfIsCancelAdd {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] [IsCancelAdd R] [IsCancelMulZero R] : IsCancelMulZero (HahnSeries Γ R)

instance HahnSeries.instNoZeroDivisors {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] : NoZeroDivisors (HahnSeries Γ R)

@[simp]

theorem HahnSeries.order_mul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {x y : HahnSeries Γ R} (hx : x ≠ 0) (hy : y ≠ 0) : (x * y).order = x.order + y.order

@[simp]

theorem HahnSeries.order_pow {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [NoZeroDivisors R] (x : HahnSeries Γ R) (n : ℕ) : (x ^ n).order = n • x.order

instance HahnSeries.instIsDomainOfIsCancelAdd {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [IsCancelAdd R] [IsDomain R] : IsDomain (HahnSeries Γ R)