lift_symm_apply

Mathlib.LinearAlgebra.Finsupp.LSum

URI: https://scilib.ai/kg/mathlib#Finsupp.lift_symm_apply

English

Sum smul identity for linear maps, i.e., the smul acts outside the sum for linear maps.

Русский

Выражение, что умножение на скаляр за пределами суммы совместимо с линейным отображением.

LaTeX

$$$$ \sum \_a (c \cdot v)_a = c \cdot \sum \_a v_a $$$$

Lean4

@[simp]
theorem lift_symm_apply (f) (x) : ((lift M R X).symm f) x = f (single x 1) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru