R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J
change A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ ⬝ (u • J) = (u • J) ⬝ (-A) ↔ Aᵀ ⬝ J = J ⬝ (-A)
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J
simp only [mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
h : Aᵀ ⬝ (u • J) = (u • J) ⬝ (-A)
⊢ Aᵀ ⬝ J = J ⬝ (-A)

case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
h : Aᵀ ⬝ J = J ⬝ (-A)
⊢ Aᵀ ⬝ (u • J) = (u • J) ⬝ (-A)
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ ⬝ (u • J) = (u • J) ⬝ (-A) ↔ Aᵀ ⬝ J = J ⬝ (-A)
constructor <;> intro h
no goals
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
h : Aᵀ ⬝ (u • J) = (u • J) ⬝ (-A)
⊢ Aᵀ ⬝ J = J ⬝ (-A)
simpa using congr_arg (fun B => u⁻¹ • B) h
no goals
case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
h : Aᵀ ⬝ J = J ⬝ (-A)
⊢ Aᵀ ⬝ (u • J) = (u • J) ⬝ (-A)
simp [h]