R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : IsSkewAdjoint J A
hB : IsSkewAdjoint J B
⊢ IsSkewAdjoint J ⁅A, B⁆
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : A ∈ skewAdjointMatricesSubmodule J
hB : B ∈ skewAdjointMatricesSubmodule J
⊢ ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J
simp only [mem_skewAdjointMatricesSubmodule] at *
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : IsSkewAdjoint J A
hB : IsSkewAdjoint J B
⊢ ⁅A, B⁆ᵀ ⬝ J = J ⬝ (-⁅A, B⁆)
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : IsSkewAdjoint J A
hB : IsSkewAdjoint J B
⊢ IsSkewAdjoint J ⁅A, B⁆
change ⁅A, B⁆ᵀ ⬝ J = J ⬝ (-⁅A, B⁆)
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hB : IsSkewAdjoint J B
hA : Aᵀ ⬝ J = J ⬝ (-A)
⊢ ⁅A, B⁆ᵀ ⬝ J = J ⬝ (-⁅A, B⁆)
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : IsSkewAdjoint J A
hB : IsSkewAdjoint J B
⊢ ⁅A, B⁆ᵀ ⬝ J = J ⬝ (-⁅A, B⁆)
change Aᵀ ⬝ J = J ⬝ (-A) at hA
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ ⬝ J = J ⬝ (-A)
hB : Bᵀ ⬝ J = J ⬝ (-B)
⊢ ⁅A, B⁆ᵀ ⬝ J = J ⬝ (-⁅A, B⁆)
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hB : IsSkewAdjoint J B
hA : Aᵀ ⬝ J = J ⬝ (-A)
⊢ ⁅A, B⁆ᵀ ⬝ J = J ⬝ (-⁅A, B⁆)
change Bᵀ ⬝ J = J ⬝ (-B) at hB
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ ⬝ J = J ⬝ (-A)
hB : Bᵀ ⬝ J = J ⬝ (-B)
⊢ ⁅A, B⁆ᵀ ⬝ J = J ⬝ (-⁅A, B⁆)
simp only [← Matrix.mul_eq_mul] at *
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ J * -B * -A - J * -A * -B = J * -(A * B - B * A)
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
rw [Matrix.lie_transpose, LieRing.of_associative_ring_bracket,
  LieRing.of_associative_ring_bracket, sub_mul, mul_assoc, mul_assoc, hA, hB, ← mul_assoc,
  ← mul_assoc, hA, hB]
no goals
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ J * -B * -A - J * -A * -B = J * -(A * B - B * A)
noncomm_ring