coeff_single_zero_smul — Mathlib

English

The coefficient of ((HahnSeries.single 0 r) • x) at a equals r times the coefficient of x at a.

Русский

Коэффициент у ((HahnSeries.single 0 r) • x) на позиции a равен r умножить на коэффициент x на позиции a.

LaTeX

$$$((\\mathrm{HahnSeries.single } 0\\ r) \\cdot x).coeff\\, a = r \\cdot x.coeff\\, a$$$

Lean4

theorem coeff_single_zero_smul {Γ} [AddCommMonoid Γ] [PartialOrder Γ] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ']
    [MulZeroClass R] [SMulWithZero R V] {r : R} {x : HahnModule Γ' R V} {a : Γ'} :
    ((of R).symm ((HahnSeries.single 0 r : HahnSeries Γ R) • x)).coeff a = r • ((of R).symm x).coeff a :=
  by
  nth_rw 1 [← zero_vadd Γ a]
  exact coeff_single_smul_vadd

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