pairSelfAdjointMatricesSubmodule — Mathlib

English

A variant of the adjoint-pair equivalence under a change of basis: the transformed J, J' and A, A' relate to the original under a fixed invertible P.

Русский

Вариант эквивалентности сопряжённости под изменением базиса: преобразованные J, J' и A, A' связаны с исходными через фиксированный обратимый P.

LaTeX

$$$(P^T J P) IsAdjointPair (P^T J P) A_1 A_2 \\iff J IsAdjointPair J (P A_1 P^{-1}) (P A_2 P^{-1}).$$$

Lean4

/-- The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to
given matrices `J`, `J₂`. -/
def pairSelfAdjointMatricesSubmodule : Submodule R (Matrix n n R) :=
  (isPairSelfAdjointSubmodule (Matrix.toLinearMap₂' R J) (Matrix.toLinearMap₂' R J₂)).map
    ((LinearMap.toMatrix' : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R) : ((n → R) →ₗ[R] n → R) →ₗ[R] Matrix n n R)

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