l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A ⬝ J l R ⬝ Aᵀ = J l R
⊢ (-A) ⬝ J l R ⬝ (-A)ᵀ = J l R
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A ∈ symplecticGroup l R
⊢ -A ∈ symplecticGroup l R
rw [mem_iff] at h⊢
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A ⬝ J l R ⬝ Aᵀ = J l R
⊢ (-A) ⬝ J l R ⬝ (-A)ᵀ = J l R
simp [h]