coe_bracket_of_module — Mathlib

English

Bracket of a LieIdeal element with a module element agrees with the bracket in the ambient Lie algebra.

Русский

Скобка элемента LieIdeal с элементом модуля совпадает с скобкой в окружающей Lie-алгебре.

LaTeX

$$$\langle x, m\rangle = \langle \iota(x), m\rangle$ where\n x \in I, m \in M, \iota: I \hookrightarrow L$$$

Lean4

@[simp]
theorem coe_bracket_of_module {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L)
    [LieRingModule L M] (x : I) (m : M) : ⁅x, m⁆ = ⁅(↑x : L), m⁆ :=
  LieSubalgebra.coe_bracket_of_module (I : LieSubalgebra R L) x m

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