l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ fromBlocks 0 1 (-1ᵀ) 0 = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ (J l R)ᵀ = -J l R
rw [J, fromBlocks_transpose, ← neg_one_smul R (fromBlocks _ _ _ _ : Matrix (l ⊕ l) (l ⊕ l) R),
  fromBlocks_smul, Matrix.transpose_zero, Matrix.transpose_one, transpose_neg]
no goals
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ fromBlocks 0 1 (-1ᵀ) 0 = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)
simp [fromBlocks]