R : Type u_1
R₁ : Type ?u.2628894
R₂ : Type ?u.2628897
M : Type ?u.2628900
M₁ : Type ?u.2628903
M₂ : Type ?u.2628906
M₁' : Type ?u.2628909
M₂' : Type ?u.2628912
n : Type u_2
m : Type ?u.2628918
n' : Type ?u.2628921
m' : Type ?u.2628924
ι : Type ?u.2628927
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ Matrix.IsAdjointPair (-J) J A₁ A₁ ↔ Matrix.IsSkewAdjoint J A₁
R : Type u_1
R₁ : Type ?u.2628894
R₂ : Type ?u.2628897
M : Type ?u.2628900
M₁ : Type ?u.2628903
M₂ : Type ?u.2628906
M₁' : Type ?u.2628909
M₂' : Type ?u.2628912
n : Type u_2
m : Type ?u.2628918
n' : Type ?u.2628921
m' : Type ?u.2628924
ι : Type ?u.2628927
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ A₁ ∈ skewAdjointMatricesSubmodule J ↔ Matrix.IsSkewAdjoint J A₁
erw [mem_pairSelfAdjointMatricesSubmodule]
no goals
R : Type u_1
R₁ : Type ?u.2628894
R₂ : Type ?u.2628897
M : Type ?u.2628900
M₁ : Type ?u.2628903
M₂ : Type ?u.2628906
M₁' : Type ?u.2628909
M₂' : Type ?u.2628912
n : Type u_2
m : Type ?u.2628918
n' : Type ?u.2628921
m' : Type ?u.2628924
ι : Type ?u.2628927
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ Matrix.IsAdjointPair (-J) J A₁ A₁ ↔ Matrix.IsSkewAdjoint J A₁
simp [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]