lieConj_apply — Mathlib

English

The Lie bracket of a matrix A with a vector v corresponds to the matrix acting on v: [A, v] = A v.

Русский

Скобка Ли между матрицей A и вектором v равна действию матрицы на вектор: [A, v] = A v.

LaTeX

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

Lean4

@[simp]
theorem lieConj_apply (P A : Matrix n n R) (h : Invertible P) : P.lieConj h A = P * A * P⁻¹ := by
  simp [LinearEquiv.conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp, LinearMap.toMatrix'_toLin']

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