of_smul — Mathlib

English

Under a left-support condition, the coefficient of the left-multiplied term equals a sum over a left-oriented VAddAntidiagonal.

Русский

При условии левой опоры коэффициент левого умножения равен сумме по левой ориентированной VAddAntidiagonal.

LaTeX

$$$((of\,R).symm \lvert x \cdot y\rvert).coeff\ a = \sum_{ij \in VAddAntidiagonal\,hs ((of R).symm y).isPWO\_support\ a} x.coeff i.fst \cdot ((of R).symm y).coeff i.snd$$$

Lean4

@[simp]
theorem of_smul [SMulZeroClass R V] (r : R) (x : HahnSeries Γ V) : (of R) (r • x) = r • (of R) x :=
  rfl

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