coeff_single_zero_mul — Mathlib

English

Reiterates the coefficient rule for right-multiplication by a single-term Hahn series.

Русский

Повторение правила коэффициентов для правого умножения на одиночный член Ханновых рядов.

LaTeX

$$$ (x \cdot \mathrm{single}\; b\; r)_{a+b} = x_a \cdot r $$$

Lean4

theorem coeff_single_zero_mul [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} :
    ((single 0 r : HahnSeries Γ R) * x).coeff a = r * x.coeff a := by rw [← add_zero a, coeff_single_mul_add, add_zero]

Похожие утверждения