coeff_single_mul_add — Mathlib

English

If the left factor is a single-term Hahn series concentrated at exponent b with coefficient r, then the coefficient at a+b in the product with x is r times the a-th coefficient of x.

Русский

Если левая часть — одиночный Ханнов ряд, сосредоточенный в степени b с коэффициентом r, то коэффициент при a+b в произведении с x равен r умножить на коэффициент x при a.

LaTeX

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

Lean4

theorem coeff_single_mul_add [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} {b : Γ} :
    (single b r * x).coeff (a + b) = r * x.coeff a :=
  by
  rw [← of_symm_smul_of_eq_mul, add_comm, ← vadd_eq_add]
  exact HahnModule.coeff_single_smul_vadd

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