m : Type ?u.2609749
n : Type ?u.2609752
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ A 0 0 * A 1 1 + -(A 0 1 * A 1 0) = A 0 0 * A 1 1 - A 0 1 * A 1 0
m : Type ?u.2609749
n : Type ?u.2609752
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ det A = A 0 0 * A 1 1 - A 0 1 * A 1 0
simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ]
no goals
m : Type ?u.2609749
n : Type ?u.2609752
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ A 0 0 * A 1 1 + -(A 0 1 * A 1 0) = A 0 0 * A 1 1 - A 0 1 * A 1 0
ring