lie_sum — Mathlib

English

The bracket of a sum on the left with a sum on the right equals the sum over all pairs: [ (∑ f_i), (∑ g_j) ] = ∑∑ [f_i, g_j].

Русский

Скобка между двумя суммами равна сумме по всем парам: [ (∑ f_i), (∑ g_j) ] = ∑∑ [f_i, g_j].

LaTeX

$$$[\sum_i f_i, \sum_j g_j] = \sum_i \sum_j [f_i, g_j]$$$

Lean4

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

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