f_lie_v_same

Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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

English

For i in the base support, the bracket [f_i, v_i] equals the unit vector u_i.

Русский

Для i из поддержки основания скобка [f_i, v_i] равна вектору u_i.

LaTeX

$$$[f_i, v_i] = u_i$$$

Lean4

theorem f_lie_v_same (i : b.support) : ⁅f i, v b i⁆ = u i :=
  by
  ext (j | j)
  · simp [f, Pi.single_apply]
  · simp [f, P.ne_zero j]

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

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

Разделы

Аффилиация

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