selfAdjointMatricesSubmodule' — Mathlib

English

Define the submodule of self-adjoint matrices with respect to a fixed bilinear form given by J.

Русский

Определим подмодуль самосопряжённых по отношению к фиксированной билинейной форме, заданной матрицей J.

LaTeX

$$$$\text{selfAdjointMatricesSubmodule}' :\; \text{Submodule}_{R_2}(\text{Matrix}_{n}(R_2)) \quad \text{with respect to } J.$$$$

Lean4

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

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