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
hA : A ∈ symplecticGroup l R
⊢ -J l R ⬝ Aᵀ ⬝ J l R ⬝ A = (-J l R) ⬝ (Aᵀ ⬝ J l R ⬝ A)
simp only [Matrix.mul_assoc, Matrix.neg_mul]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ ⬝ J l R ⬝ A = J l R
⊢ (-J l R) ⬝ (Aᵀ ⬝ J l R ⬝ A) = (-J l R) ⬝ 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
hA : A ∈ symplecticGroup l R
⊢ (-J l R) ⬝ (Aᵀ ⬝ J l R ⬝ A) = (-J l R) ⬝ J l R
rw [mem_iff'] at hA
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
hA : Aᵀ ⬝ J l R ⬝ A = J l R
⊢ (-J l R) ⬝ (Aᵀ ⬝ J l R ⬝ A) = (-J l R) ⬝ J l R
rw [hA]
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
hA : A ∈ symplecticGroup l R
⊢ (-J l R) ⬝ J l R = -1 • J l R ⬝ J l R
simp only [Matrix.neg_mul, neg_smul, one_smul]
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
hA : A ∈ symplecticGroup l R
⊢ -1 • J l R ⬝ J l R = -1 • -1
rw [J_squared]
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
hA : A ∈ symplecticGroup l R
⊢ -1 • -1 = 1
simp only [neg_smul_neg, one_smul]