Theorems · Theorem · group theory

SymplecticGroup.transpose_mem

∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R}, A ∈ Matrix.symplecticGroup l R → A.transpose ∈ Matrix.symplecticGroup l R

Defined in

Mathlib.LinearAlgebra.SymplecticGroup

Cited by

2 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeCommRing