heval_mul — Mathlib

English

The hsum of the product of two power-series families equals the hsum of their convolution.

Русский

Сумма по степенным сериям произведения двух семейств равна сумме их свёртки.

LaTeX

$$ (HahnSeries.SummableFamily.powerSeriesFamily x (a * b)).hsum = ((HahnSeries.SummableFamily.powerSeriesFamily x a).mul (HahnSeries.SummableFamily.powerSeriesFamily x b)).hsum$$

Lean4

theorem heval_mul {a b : PowerSeries R} : heval x (a * b) = heval x a * heval x b :=
  map_mul (heval x) a b

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