f_mem_lieAlgebra

Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

URI: https://scilib.ai/kg/mathlib#RootPairing.GeckConstruction.f_mem_lieAlgebra

English

For every i ∈ b.support, the matrix f(i) lies in the Lie algebra constructed from the root data.

Русский

Для каждого i ∈ b.support матрица f(i) принадлежит Ли-алгебре, построенной по данным корней.

LaTeX

$$$f(i) \in \text{lieAlgebra}(b)$$$

Lean4

theorem f_mem_lieAlgebra [Fintype ι] [DecidableEq ι] (i : b.support) : f i ∈ lieAlgebra b :=
  LieSubalgebra.subset_lieSpan <| by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru