sum_lie

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#sum_lie

English

The bracket with a finite sum distributes over the sum: [a, ∑ f_i] = ∑ [a, f_i].

Русский

Скобка вокруг суммы распределяется по сумме: [a, ∑ f_i] = ∑ [a, f_i].

LaTeX

$$$[a, \sum_{i \in s} f_i] = \sum_{i \in s} [a, f_i]$$$

Lean4

theorem sum_lie (s : Finset ι) (f : ι → L) (m : M) : ⁅∑ i ∈ s, f i, m⁆ = ∑ i ∈ s, ⁅f i, m⁆ :=
  map_sum ((LieRingModule.toEnd L M).flip m) f s

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

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

Разделы

Аффилиация

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