lie_apply

Mathlib.Algebra.Lie.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.lie_apply

English

The Lie bracket of a matrix A with a vector v coincides with the action A·v.

Русский

Скобка Ли между матрицей A и вектором v совпадает с действием A·v.

LaTeX

$$$\\,[A,v\\] = A \\cdot v.$$$

Lean4

@[simp]
theorem lie_apply (A : Matrix n n R) (v : n → R) : ⁅A, v⁆ = A *ᵥ v :=
  rfl

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

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

Разделы

Аффилиация

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