smul_apply — Mathlib

English

The hsum of an image under a linear isomorphism equals the image of the hsum under that isomorphism.

Русский

Сумма по изображению линейного изоморфизма равна изображению суммы этим изоморфизмом.

LaTeX

$$$ (\mathrm{hsum}\, s) = \mathrm{hsum}\, (s) $$$

Lean4

@[simp]
theorem smul_apply {x : HahnSeries Γ R} {s : SummableFamily Γ' V α} {a : α} :
    (x • s) a = (of R).symm (x • of R (s a)) :=
  rfl

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