skewAdjointMatricesSubmodule' — Mathlib

English

Define the skew-adjoint submodule using pairSelfAdjointMatricesSubmodule with −J and J.

Русский

Определим подмодуль skew-adjoint через pairSelfAdjointMatricesSubmodule с −J и J.

LaTeX

$$$$\text{skewAdjointMatricesSubmodule}' : = \text{pairSelfAdjointMatricesSubmodule}(-J, J).$$$$

Lean4

/-- The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to
the matrix `J`. -/
def skewAdjointMatricesSubmodule' : Submodule R₂ (Matrix n n R₂) :=
  pairSelfAdjointMatricesSubmodule (-J) J

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