n : Type u_1
p : Type ?u.30314
q : Type ?u.30317
l : Type ?u.30320
R : Type u₂
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix n n R
⊢ IsSkewAdjoint 1 A ↔ Aᵀ = -A
n : Type u_1
p : Type ?u.30314
q : Type ?u.30317
l : Type ?u.30320
R : Type u₂
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix n n R
⊢ A ∈ so n R ↔ Aᵀ = -A
rw [so, mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule]
no goals
n : Type u_1
p : Type ?u.30314
q : Type ?u.30317
l : Type ?u.30320
R : Type u₂
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix n n R
⊢ IsSkewAdjoint 1 A ↔ Aᵀ = -A
simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, Matrix.mul_one, Matrix.one_mul]