actionAsEndoMapBracket — Mathlib

English

The quotient M/N carries a Lie bracket action of L defined by [x, m̄] = actionOfEndo(x)(m̄).

Русский

Фактор-модуль M/N имеет скобочное действие Ли над L: [x, m̄] = действие скобкой на косет m̄.

LaTeX

$$instance Bracket L (M ⧸ N) :=$$

Lean4

/-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there is
a natural bracket action of `L` on the quotient `M/N`. -/
instance actionAsEndoMapBracket : Bracket L (M ⧸ N) :=
  ⟨fun x n => actionAsEndoMap N x n⟩

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