lieIdeal_oper_eq_span — Mathlib

English

For a Lie submodule N and Lie ideal I, the Lie bracket [I,N] considered as a submodule of M equals the linear span of all brackets [x,n] with x ∈ I and n ∈ N.

Русский

Для подмодуля N и Ли-идеала I, скобка [I,N] как подмодуль M равна линейному охвату всех скобок [x,n] при x ∈ I, n ∈ N.

LaTeX

$$$$ (\,[I,N]\,\text{as Submodule}\, M) = \operatorname{span}_R\{ [x,n] \mid x \in I, n \in N \}. $$$$

Lean4

theorem lieIdeal_oper_eq_span : ⁅I, N⁆ = lieSpan R L {⁅(x : L), (n : M)⁆ | (x : I) (n : N)} :=
  rfl

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