IsSkewAdjoint — Mathlib

English

Two ways of expressing adjointness are equivalent: the matrix-based adjoint pair corresponds to the adjoint pair of the associated linear maps under a chosen basis.

Русский

Сопряжённость можно одинаково выразить через матрицу или через линейные отображения: существование пары сопряжённых линейных отображений соответствует сопряжённости матриц при заданном базисе.

LaTeX

$$$\\text{Matrix IsAdjointPair } J J' A A' \\;\\Longleftrightarrow\\; \\text{LinearMap IsAdjointPair } (\\text{toLin}' A)(\\text{toLin}' A').$$$

Lean4

/-- The condition for a square matrix `A` to be skew-adjoint with respect to the square matrix
`J`. -/
protected def IsSkewAdjoint :=
  Matrix.IsAdjointPair J J A₁ (-A₁)

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