English
If A,B are skew-adjoint with respect to a fixed bilinear form J, then their Lie bracket is again skew-adjoint with respect to J.
Русский
Если A,B кососопряжённы относительно заданной билинейной формы J, то их скобка по Ли снова кососопряжена относительно J.
LaTeX
$$$A,B \in skewAdjointMatricesSubmodule J \Rightarrow [A,B] \in skewAdjointMatricesSubmodule J$$$
Lean4
theorem isSkewAdjoint_bracket {A B : Matrix n n R} (hA : A ∈ skewAdjointMatricesSubmodule J)
(hB : B ∈ skewAdjointMatricesSubmodule J) : ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J :=
by
simp only [mem_skewAdjointMatricesSubmodule] at *
change ⁅A, B⁆ᵀ * J = J * (-⁅A, B⁆)
change Aᵀ * J = J * (-A) at hA
change Bᵀ * J = J * (-B) at hB
rw [Matrix.lie_transpose, LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket, sub_mul,
mul_assoc, mul_assoc, hA, hB, ← mul_assoc, ← mul_assoc, hA, hB]
noncomm_ring
