mem_skewAdjointMatricesSubmodule'

English

For matrices J, define the skew-adjoint submodule; membership is equivalent to J.IsSkewAdjoint A.

Русский

Для матриц J определить подмодуль skew-adjoint; принадлежность эквивалентна J.IsSkewAdjoint A.

LaTeX

$$$$A \in skewAdjointMatricesSubmodule J \iff J.IsSkewAdjoint A.$$$$

Lean4

theorem mem_skewAdjointMatricesSubmodule' : A ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A := by
  simp only [mem_skewAdjointMatricesSubmodule]

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