mem_toLieSubalgebra_iff — Mathlib

English

Equivalences of membership with a Lie subalgebra represented as a span of triple generators.

Русский

Эквивалентность принадлежности под Ли-подалгебре, выражаемая как линейная комбинация порождающих тройки.

LaTeX

$$IsSl2Triple.mem_toLieSubalgebra_iff$$

Lean4

theorem mem_toLieSubalgebra_iff {x : L} {t : IsSl2Triple h e f} :
    x ∈ t.toLieSubalgebra R ↔ ∃ c₁ c₂ c₃ : R, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ := by
  simp_rw [t.lie_e_f, toLieSubalgebra, ← LieSubalgebra.mem_toSubmodule, Submodule.mem_span_triple, eq_comm]

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