lie_transpose — Mathlib

English

For square matrices, the transpose of the Lie bracket satisfies a natural compatibility with transpose: ( [A,B] )^T = [B^T, A^T].

Русский

Для квадратных матриц транспонирование совместимо со скобкой Ли: ( [A,B] )^T = [B^T, A^T].

LaTeX

$$$([A,B])^{T} = [B^{T}, A^{T}]$$$

Lean4

theorem lie_transpose (A B : Matrix n n R) : ⁅A, B⁆ᵀ = ⁅Bᵀ, Aᵀ⁆ :=
  show (A * B - B * A)ᵀ = Bᵀ * Aᵀ - Aᵀ * Bᵀ by simp

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