Documentation

Mathlib.RingTheory.HahnSeries.Addition

Additive properties of Hahn series #

If Γ is ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered. With further structure on R and Γ, we can add further structure on HahnSeries Γ R. When R has an addition operation, HahnSeries Γ R also has addition by adding coefficients.

Main Definitions #

If R is a (commutative) additive monoid or group, then so is HahnSeries Γ R.

References #

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

instance HahnSeries.instSMul {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Zero V] [SMulZeroClass R V] :

SMul R (HahnSeries Γ V)

Equations

@[simp]

theorem HahnSeries.coeff_smul' {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Zero V] [SMulZeroClass R V] (r : R) (x : HahnSeries Γ V) :

(r • x).coeff = r • x.coeff

@[simp]

theorem HahnSeries.coeff_smul {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Zero V] [SMulZeroClass R V] {r : R} {x : HahnSeries Γ V} {a : Γ} :

(r • x).coeff a = r • x.coeff a

@[deprecated HahnSeries.coeff_smul (since := "2025-01-31")]

theorem HahnSeries.smul_coeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Zero V] [SMulZeroClass R V] {r : R} {x : HahnSeries Γ V} {a : Γ} :

(r • x).coeff a = r • x.coeff a

Alias of HahnSeries.coeff_smul.

instance HahnSeries.instSMulZeroClass {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Zero V] [SMulZeroClass R V] :

SMulZeroClass R (HahnSeries Γ V)

Equations

theorem HahnSeries.orderTop_smul_not_lt {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Zero V] [SMulZeroClass R V] (r : R) (x : HahnSeries Γ V) :

¬(r • x).orderTop < x.orderTop

theorem HahnSeries.order_smul_not_lt {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Zero V] [SMulZeroClass R V] [Zero Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :

¬(r • x).order < x.order

theorem HahnSeries.le_order_smul {R : Type u_3} {V : Type u_8} [Zero V] [SMulZeroClass R V] {Γ : Type u_9} [Zero Γ] [LinearOrder Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :

x.order ≤ (r • x).order

theorem HahnSeries.truncLT_smul {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Zero V] [SMulZeroClass R V] [DecidableLT Γ] (c : Γ) (r : R) (x : HahnSeries Γ V) :

(truncLT c) (r • x) = r • (truncLT c) x

instance HahnSeries.instAdd {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] :

Add (HahnSeries Γ R)

Equations

@[simp]

theorem HahnSeries.coeff_add' {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x y : HahnSeries Γ R) :

(x + y).coeff = x.coeff + y.coeff

@[deprecated HahnSeries.coeff_add' (since := "2025-01-31")]

theorem HahnSeries.add_coeff' {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x y : HahnSeries Γ R) :

(x + y).coeff = x.coeff + y.coeff

Alias of HahnSeries.coeff_add'.

theorem HahnSeries.coeff_add {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] {x y : HahnSeries Γ R} {a : Γ} :

(x + y).coeff a = x.coeff a + y.coeff a

@[simp]

theorem HahnSeries.single_add {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (a : Γ) (r s : R) :

(single a) (r + s) = (single a) r + (single a) s

@[deprecated HahnSeries.coeff_add (since := "2025-01-31")]

theorem HahnSeries.add_coeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] {x y : HahnSeries Γ R} {a : Γ} :

(x + y).coeff a = x.coeff a + y.coeff a

Alias of HahnSeries.coeff_add.

instance HahnSeries.instAddMonoid {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] :

AddMonoid (HahnSeries Γ R)

Equations

theorem HahnSeries.coeff_nsmul {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] {x : HahnSeries Γ R} {n : ℕ} :

(n • x).coeff = n • x.coeff

@[deprecated HahnSeries.coeff_nsmul (since := "2025-01-31")]

theorem HahnSeries.nsmul_coeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] {x : HahnSeries Γ R} {n : ℕ} :

(n • x).coeff = n • x.coeff

Alias of HahnSeries.coeff_nsmul.

@[simp]

theorem HahnSeries.map_add {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [AddMonoid R] [AddMonoid S] (f : R →+ S) {x y : HahnSeries Γ R} :

(x + y).map f = x.map f + y.map f

def HahnSeries.addOppositeEquiv {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] :

HahnSeries Γ Rᵃᵒᵖ ≃+ (HahnSeries Γ R)ᵃᵒᵖ

addOppositeEquiv is an additive monoid isomorphism between Hahn series over Γ with coefficients in the opposite additive monoid Rᵃᵒᵖ and the additive opposite of Hahn series over Γ with coefficients R.

Equations

Instances For

theorem HahnSeries.addOppositeEquiv_apply {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x : HahnSeries Γ Rᵃᵒᵖ) :

addOppositeEquiv x = AddOpposite.op { coeff := fun (a : Γ) => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }

theorem HahnSeries.addOppositeEquiv_symm_apply_coeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x : (HahnSeries Γ R)ᵃᵒᵖ) (a : Γ) :

(addOppositeEquiv.symm x).coeff a = AddOpposite.op ((AddOpposite.unop x).coeff a)

@[simp]

theorem HahnSeries.addOppositeEquiv_support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x : HahnSeries Γ Rᵃᵒᵖ) :

(AddOpposite.unop (addOppositeEquiv x)).support = x.support

@[simp]

theorem HahnSeries.addOppositeEquiv_symm_support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x : (HahnSeries Γ R)ᵃᵒᵖ) :

(addOppositeEquiv.symm x).support = (AddOpposite.unop x).support

@[simp]

theorem HahnSeries.addOppositeEquiv_orderTop {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x : HahnSeries Γ Rᵃᵒᵖ) :

(AddOpposite.unop (addOppositeEquiv x)).orderTop = x.orderTop

@[simp]

theorem HahnSeries.addOppositeEquiv_symm_orderTop {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x : (HahnSeries Γ R)ᵃᵒᵖ) :

(addOppositeEquiv.symm x).orderTop = (AddOpposite.unop x).orderTop

@[simp]

theorem HahnSeries.addOppositeEquiv_leadingCoeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x : HahnSeries Γ Rᵃᵒᵖ) :

(AddOpposite.unop (addOppositeEquiv x)).leadingCoeff = AddOpposite.unop x.leadingCoeff

@[simp]

theorem HahnSeries.addOppositeEquiv_symm_leadingCoeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (x : (HahnSeries Γ R)ᵃᵒᵖ) :

(addOppositeEquiv.symm x).leadingCoeff = AddOpposite.op (AddOpposite.unop x).leadingCoeff

theorem HahnSeries.support_add_subset {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] {x y : HahnSeries Γ R} :

(x + y).support ⊆ x.support ∪ y.support

theorem HahnSeries.min_le_min_add {R : Type u_3} [AddMonoid R] {Γ : Type u_8} [LinearOrder Γ] {x y : HahnSeries Γ R} (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x + y ≠ 0) :

min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯

theorem HahnSeries.min_orderTop_le_orderTop_add {R : Type u_3} [AddMonoid R] {Γ : Type u_8} [LinearOrder Γ] {x y : HahnSeries Γ R} :

min x.orderTop y.orderTop ≤ (x + y).orderTop

theorem HahnSeries.min_order_le_order_add {R : Type u_3} [AddMonoid R] {Γ : Type u_8} [Zero Γ] [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : x + y ≠ 0) :

min x.order y.order ≤ (x + y).order

theorem HahnSeries.orderTop_add_eq_left {R : Type u_3} [AddMonoid R] {Γ : Type u_8} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : x.orderTop < y.orderTop) :

(x + y).orderTop = x.orderTop

theorem HahnSeries.orderTop_add_eq_right {R : Type u_3} [AddMonoid R] {Γ : Type u_8} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : y.orderTop < x.orderTop) :

(x + y).orderTop = y.orderTop

theorem HahnSeries.leadingCoeff_add_eq_left {R : Type u_3} [AddMonoid R] {Γ : Type u_8} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : x.orderTop < y.orderTop) :

(x + y).leadingCoeff = x.leadingCoeff

theorem HahnSeries.leadingCoeff_add_eq_right {R : Type u_3} [AddMonoid R] {Γ : Type u_8} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : y.orderTop < x.orderTop) :

(x + y).leadingCoeff = y.leadingCoeff

theorem HahnSeries.ne_zero_of_eq_add_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] [Zero Γ] {x y : HahnSeries Γ R} (hxy : x = y + (single x.order) x.leadingCoeff) (hy : y ≠ 0) :

x ≠ 0

theorem HahnSeries.coeff_order_of_eq_add_single {Γ : Type u_1} [PartialOrder Γ] {R : Type u_8} [AddCancelCommMonoid R] [Zero Γ] {x y : HahnSeries Γ R} (hxy : x = y + (single x.order) x.leadingCoeff) (h : x ≠ 0) :

y.coeff x.order = 0

theorem HahnSeries.order_lt_order_of_eq_add_single {R : Type u_8} {Γ : Type u_9} [LinearOrder Γ] [Zero Γ] [AddCancelCommMonoid R] {x y : HahnSeries Γ R} (hxy : x = y + (single x.order) x.leadingCoeff) (hy : y ≠ 0) :

x.order < y.order

def HahnSeries.single.addMonoidHom {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (a : Γ) :

R →+ HahnSeries Γ R

single as an additive monoid/group homomorphism

Equations

Instances For

@[simp]

theorem HahnSeries.single.addMonoidHom_apply_coeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (a : Γ) (r : R) (j : Γ) :

((addMonoidHom a) r).coeff j = Pi.single a r j

def HahnSeries.coeff.addMonoidHom {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (g : Γ) :

HahnSeries Γ R →+ R

coeff g as an additive monoid/group homomorphism

Equations

Instances For

@[simp]

theorem HahnSeries.coeff.addMonoidHom_apply {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] (g : Γ) (f : HahnSeries Γ R) :

(addMonoidHom g) f = f.coeff g

theorem HahnSeries.embDomain_add {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] [PartialOrder Γ'] (f : Γ ↪o Γ') (x y : HahnSeries Γ R) :

embDomain f (x + y) = embDomain f x + embDomain f y

theorem HahnSeries.truncLT_add {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddMonoid R] [DecidableLT Γ] (c : Γ) (x y : HahnSeries Γ R) :

(truncLT c) (x + y) = (truncLT c) x + (truncLT c) y

instance HahnSeries.instAddCommMonoid {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid R] :

AddCommMonoid (HahnSeries Γ R)

Equations

@[simp]

theorem HahnSeries.coeff_sum {Γ : Type u_1} {R : Type u_3} {α : Type u_7} [PartialOrder Γ] [AddCommMonoid R] {s : Finset α} {x : α → HahnSeries Γ R} (g : Γ) :

(∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g

instance HahnSeries.instNeg {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] :

Neg (HahnSeries Γ R)

Equations

@[simp]

theorem HahnSeries.coeff_neg' {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] (x : HahnSeries Γ R) :

(-x).coeff = -x.coeff

@[deprecated HahnSeries.coeff_neg' (since := "2025-01-31")]

theorem HahnSeries.neg_coeff' {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] (x : HahnSeries Γ R) :

(-x).coeff = -x.coeff

Alias of HahnSeries.coeff_neg'.

theorem HahnSeries.coeff_neg {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} {a : Γ} :

(-x).coeff a = -x.coeff a

@[deprecated HahnSeries.coeff_neg (since := "2025-01-31")]

theorem HahnSeries.neg_coeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} {a : Γ} :

(-x).coeff a = -x.coeff a

Alias of HahnSeries.coeff_neg.

instance HahnSeries.instSub {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] :

Sub (HahnSeries Γ R)

Equations

@[simp]

theorem HahnSeries.coeff_sub' {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] (x y : HahnSeries Γ R) :

(x - y).coeff = x.coeff - y.coeff

@[deprecated HahnSeries.coeff_sub' (since := "2025-01-31")]

theorem HahnSeries.sub_coeff' {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] (x y : HahnSeries Γ R) :

(x - y).coeff = x.coeff - y.coeff

Alias of HahnSeries.coeff_sub'.

theorem HahnSeries.coeff_sub {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] {x y : HahnSeries Γ R} {a : Γ} :

(x - y).coeff a = x.coeff a - y.coeff a

@[deprecated HahnSeries.coeff_sub (since := "2025-01-31")]

theorem HahnSeries.sub_coeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] {x y : HahnSeries Γ R} {a : Γ} :

(x - y).coeff a = x.coeff a - y.coeff a

Alias of HahnSeries.coeff_sub.

instance HahnSeries.instAddGroup {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] :

AddGroup (HahnSeries Γ R)

Equations

@[simp]

theorem HahnSeries.single_sub {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] (a : Γ) (r s : R) :

(single a) (r - s) = (single a) r - (single a) s

@[simp]

theorem HahnSeries.single_neg {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] (a : Γ) (r : R) :

(single a) (-r) = -(single a) r

@[simp]

theorem HahnSeries.support_neg {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} :

(-x).support = x.support

@[simp]

theorem HahnSeries.map_neg {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [AddGroup R] [AddGroup S] (f : R →+ S) {x : HahnSeries Γ R} :

(-x).map f = -x.map f

@[simp]

theorem HahnSeries.orderTop_neg {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} :

(-x).orderTop = x.orderTop

@[simp]

theorem HahnSeries.order_neg {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] [Zero Γ] {f : HahnSeries Γ R} :

(-f).order = f.order

theorem HahnSeries.leadingCoeff_neg {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} :

(-x).leadingCoeff = -x.leadingCoeff

@[simp]

theorem HahnSeries.map_sub {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [AddGroup R] [AddGroup S] (f : R →+ S) {x y : HahnSeries Γ R} :

(x - y).map f = x.map f - y.map f

theorem HahnSeries.min_orderTop_le_orderTop_sub {R : Type u_3} [AddGroup R] {Γ : Type u_8} [LinearOrder Γ] {x y : HahnSeries Γ R} :

min x.orderTop y.orderTop ≤ (x - y).orderTop

theorem HahnSeries.orderTop_sub {R : Type u_3} [AddGroup R] {Γ : Type u_8} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : x.orderTop < y.orderTop) :

(x - y).orderTop = x.orderTop

theorem HahnSeries.leadingCoeff_sub {R : Type u_3} [AddGroup R] {Γ : Type u_8} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : x.orderTop < y.orderTop) :

(x - y).leadingCoeff = x.leadingCoeff

instance HahnSeries.instAddCommGroup {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommGroup R] :

AddCommGroup (HahnSeries Γ R)

Equations

instance HahnSeries.instDistribMulAction {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Monoid R] [AddMonoid V] [DistribMulAction R V] :

DistribMulAction R (HahnSeries Γ V)

Equations

instance HahnSeries.instIsScalarTower {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Monoid R] [AddMonoid V] [DistribMulAction R V] {S : Type u_9} [Monoid S] [DistribMulAction S V] [SMul R S] [IsScalarTower R S V] :

IsScalarTower R S (HahnSeries Γ V)

instance HahnSeries.instSMulCommClass {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] {V : Type u_8} [Monoid R] [AddMonoid V] [DistribMulAction R V] {S : Type u_9} [Monoid S] [DistribMulAction S V] [SMulCommClass R S V] :

SMulCommClass R S (HahnSeries Γ V)

instance HahnSeries.instModule {Γ : Type u_1} {R : Type u_3} {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] :

Module R (HahnSeries Γ V)

Equations

def HahnSeries.single.linearMap {Γ : Type u_1} {R : Type u_3} {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] (a : Γ) :

V →ₗ[R] HahnSeries Γ V

single as a linear map

Equations

Instances For

@[simp]

theorem HahnSeries.single.linearMap_apply {Γ : Type u_1} {R : Type u_3} {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] (a : Γ) (a✝ : V) :

(linearMap a) a✝ = (↑(addMonoidHom a)).toFun a✝

def HahnSeries.coeff.linearMap {Γ : Type u_1} {R : Type u_3} {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] (g : Γ) :

HahnSeries Γ V →ₗ[R] V

coeff g as a linear map

Equations

Instances For

@[simp]

theorem HahnSeries.coeff.linearMap_apply {Γ : Type u_1} {R : Type u_3} {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] (g : Γ) (a✝ : HahnSeries Γ V) :

(linearMap g) a✝ = (↑(addMonoidHom g)).toFun a✝

@[simp]

theorem HahnSeries.map_smul {Γ : Type u_1} {R : Type u_3} {U : Type u_5} {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid U] [Module R U] (f : U →ₗ[R] V) {r : R} {x : HahnSeries Γ U} :

(r • x).map f = r • x.map f

def HahnSeries.ofFinsuppLinearMap {Γ : Type u_1} (R : Type u_3) {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] :

(Γ →₀ V) →ₗ[R] HahnSeries Γ V

ofFinsupp as a linear map.

Equations

Instances For

@[simp]

theorem HahnSeries.coeff_ofFinsuppLinearMap {Γ : Type u_1} (R : Type u_3) {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] (f : Γ →₀ V) (a : Γ) :

((ofFinsuppLinearMap R) f).coeff a = f a

theorem HahnSeries.embDomain_smul {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Semiring R] [PartialOrder Γ'] (f : Γ ↪o Γ') (r : R) (x : HahnSeries Γ R) :

embDomain f (r • x) = r • embDomain f x

def HahnSeries.embDomainLinearMap {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Semiring R] [PartialOrder Γ'] (f : Γ ↪o Γ') :

HahnSeries Γ R →ₗ[R] HahnSeries Γ' R

Extending the domain of Hahn series is a linear map.

Equations

Instances For

@[simp]

theorem HahnSeries.embDomainLinearMap_apply {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Semiring R] [PartialOrder Γ'] (f : Γ ↪o Γ') (a✝ : HahnSeries Γ R) :

(embDomainLinearMap f) a✝ = embDomain f a✝

def HahnSeries.truncLTLinearMap {Γ : Type u_1} (R : Type u_3) {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] [DecidableLT Γ] (c : Γ) :

HahnSeries Γ V →ₗ[R] HahnSeries Γ V

HahnSeries.truncLT as a linear map.

Equations

Instances For

@[simp]

theorem HahnSeries.coe_truncLTLinearMap {Γ : Type u_1} (R : Type u_3) {V : Type u_6} [PartialOrder Γ] [Semiring R] [AddCommMonoid V] [Module R V] [DecidableLT Γ] (c : Γ) :

⇑(truncLTLinearMap R c) = ⇑(truncLT c)