coeff_mul_single_zero — Mathlib

English

The same coefficient rule holds for multiplying on the right by a single-term Hahn series.

Русский

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

LaTeX

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

Lean4

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

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