mem_so — Mathlib

English

An array A lies in so n R iff A^T = -A.

Русский

Матрица A принадлежит so_n(R) тогда и только тогда, когда A^T = -A.

LaTeX

$$$$ A \in so_n(R) \iff A^T = -A. $$$$

Lean4

@[simp]
theorem mem_so [Fintype n] (A : Matrix n n R) : A ∈ so n R ↔ Aᵀ = -A :=
  by
  rw [so, mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule]
  simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, Matrix.mul_one, Matrix.one_mul]

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