sum_lie_sum — Mathlib

English

There is a LieRingModule structure on L acting on the space of linear maps M →ᴿ N, with bracket defined by x acting on f as [x,f](m) = [x,f(m)] − f([x,m]).

Русский

Существует структура LieRingModule на L, действующем на пространство линейных отображений M →ᴿ N, скобка задаётся как [x,f](m) = [x,f(m)] − f([x,m]).

LaTeX

$$$\text{LieRingModule } L (M \to_R N):\quad [x,f](m) = [x,f(m)] - f([x,m])$$$

Lean4

theorem sum_lie_sum {κ : Type*} (s : Finset ι) (t : Finset κ) (f : ι → L) (g : κ → M) :
    ⁅(∑ i ∈ s, f i), ∑ j ∈ t, g j⁆ = ∑ i ∈ s, ∑ j ∈ t, ⁅f i, g j⁆ := by simp_rw [sum_lie, lie_sum]

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