selfAdjointMatricesSubmodule — Mathlib

English

An element A₁ belongs to the self-adjoint submodule corresponding to J if and only if A₁ is self-adjoint with respect to the pair (J, J).

Русский

Элемент A₁ принадлежит подпространству самопряжённых относительно J, если и только если A₁ самопряжён по паре (J,J).

LaTeX

$$$A_1 \\in \\text{selfAdjointMatricesSubmodule}(J) \\iff J IsSelfAdjoint A_1.$$$

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

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