English
If f and g are skew-adjoint endomorphisms with respect to a bilinear form B, then their commutator [f,g] is also skew-adjoint with respect to B.
Русский
Если f и g — кососопряжённые эндоморфизмы по отношению к билинейной форме B, то их коммутатор [f,g] тоже кососопряжён по отношению к B.
LaTeX
$$$f,g \in B.skewAdjointSubmodule \implies [f,g] \in B.skewAdjointSubmodule$$$
Lean4
theorem isSkewAdjoint_bracket {f g : Module.End R M} (hf : f ∈ B.skewAdjointSubmodule)
(hg : g ∈ B.skewAdjointSubmodule) : ⁅f, g⁆ ∈ B.skewAdjointSubmodule :=
by
rw [mem_skewAdjointSubmodule] at *
have hfg : IsAdjointPair B B (f * g) (g * f) := by rw [← neg_mul_neg g f]; exact hg.comp hf
have hgf : IsAdjointPair B B (g * f) (f * g) := by rw [← neg_mul_neg f g]; exact hf.comp hg
change IsAdjointPair B B (f * g - g * f) (-(f * g - g * f)); rw [neg_sub]
exact hfg.sub hgf
