HahnSeries.add_coeff
theorem HahnSeries.add_coeff :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] {x y : HahnSeries Γ R} {a : Γ},
(x + y).coeff a = x.coeff a + y.coeff a
This theorem is about Hahn series. It states that for any two Hahn series `x` and `y` over a partially ordered set `Γ` and an additive monoid `R`, the coefficient of a term with index `a` in the sum of `x` and `y` is equal to the sum of the coefficients of the term with index `a` in `x` and `y`. Formally, `(x + y).coeff a = x.coeff a + y.coeff a`. It essentially describes the distributive property of addition over the coefficients of Hahn Series.
More concisely: For Hahn series x and y over a partially ordered set Γ and an additive monoid R, the coefficient of index a in their sum is equal to the sum of the coefficients of index a in x and y: (x + y).coeff a = x.coeff a + y.coeff a.
|
HahnSeries.support_neg
theorem HahnSeries.support_neg :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddGroup R] {x : HahnSeries Γ R},
(-x).support = x.support
This theorem states that for all types `Γ` and `R`, where `Γ` is a partially ordered set and `R` is an additive group, and for any `x` of type `HahnSeries Γ R`, the support of the negation of `x` is equal to the support of `x`. In other words, the set of indices with non-zero coefficients remains the same when a Hahn series is negated.
More concisely: For any Hahn series `x` of type `HahnSeries Γ R` over a partially ordered set `Γ` and an additive group `R`, the support of `x` is equal to the support of its negation.
|