transpose_mem_iff — Mathlib

English

Membership of a matrix in the symplectic group is preserved by transposition, and vice versa.

Русский

Принадлежность матрицы к симплектической группе сохраняется при транспонировании и обратно.

LaTeX

$$Aᵀ ∈ Sp(l,R) ↔ A ∈ Sp(l,R)$$

Lean4

@[simp]
theorem transpose_mem_iff : Aᵀ ∈ symplecticGroup l R ↔ A ∈ symplecticGroup l R :=
  ⟨fun hA => by simpa using transpose_mem hA, transpose_mem⟩

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