HahnSeries.single_zero_mul_eq_smul
theorem HahnSeries.single_zero_mul_eq_smul :
∀ {Γ : Type u_1} {R : Type u_2} [inst : OrderedCancelAddCommMonoid Γ] [inst_1 : Semiring R] {r : R}
{x : HahnSeries Γ R}, (HahnSeries.single 0) r * x = r • x
This theorem states that for any given type `Γ` with an ordered cancel addition commutative monoid structure, and another type `R` with a semiring structure, along with any element `r` of type `R` and a Hahn series `x` of type `HahnSeries Γ R`, the product of `r` (interpreted as a Hahn series where `r` is the coefficient at `0` and `0` is the coefficient everywhere else) and `x` equals `r` scaled by `x`. In other words, this theorem asserts that multiplication by a scalar in Hahn series corresponds to scalar multiplication.
More concisely: For any ordered commutative monoid type `Γ`, semiring type `R`, element `r` in `R`, and Hahn series `x` of type `HahnSeries Γ R`, the product of `r` as a Hahn series and `x` equals `r` scaled by `x`, i.e., `r * x = (r * 1) * x`.
|
HahnSeries.single_mul_single
theorem HahnSeries.single_mul_single :
∀ {Γ : Type u_1} {R : Type u_2} [inst : OrderedCancelAddCommMonoid Γ] [inst_1 : NonUnitalNonAssocSemiring R]
{a b : Γ} {r s : R}, (HahnSeries.single a) r * (HahnSeries.single b) s = (HahnSeries.single (a + b)) (r * s)
The theorem `HahnSeries.single_mul_single` states that for any ordered cancel-additive commutative monoid `Γ`, non-unital non-associative semiring `R`, elements `a` and `b` from `Γ`, and elements `r` and `s` from `R`, the product of the Hahn series `HahnSeries.single a r` and `HahnSeries.single b s` is the Hahn series `HahnSeries.single (a + b) (r * s)`. In other words, it states that the multiplication of two Hahn series, each having a single nonzero coefficient, results in a new Hahn series with a single nonzero coefficient at the sum of the indices and the product of the coefficients.
More concisely: For any ordered cancel-additive commutative monoid Γ, non-unital non-associative semiring R, and elements a, b from Γ, and r, s from R, the product of the Hahn series HahnSeries.single a r and HahnSeries.single b s is equal to HahnSeries.single (a + b) (r * s).
|