l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (0 ⬝ 0 + (-1) ⬝ 1) (0 ⬝ (-1) + (-1) ⬝ 0) (1 ⬝ 0 + 0 ⬝ 1) (1 ⬝ (-1) + 0 ⬝ 0) = -1
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ J l R ⬝ J l R = -1
rw [J, fromBlocks_multiply]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (-1) 0 0 (-1) = -1
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (0 ⬝ 0 + (-1) ⬝ 1) (0 ⬝ (-1) + (-1) ⬝ 0) (1 ⬝ 0 + 0 ⬝ 1) (1 ⬝ (-1) + 0 ⬝ 0) = -1
simp only [Matrix.zero_mul, Matrix.neg_mul, zero_add, neg_zero, Matrix.one_mul, add_zero]
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (-1) 0 0 (-1) = -1
rw [← neg_zero, ← Matrix.fromBlocks_neg, ← fromBlocks_one]