Theorem: MatrixCookbook.eq_25 (MatrixCookbook/1Basic.lean)

State before:
ι : Type ?u.30876
R : Type u_1
m : Type ?u.30882
n : Type ?u.30885
p : Type ?u.30888
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ (1 + A).det = 1 + A.det + A.trace
Tactic:
simp [det_fin_two, trace_fin_two]
State after:
ι : Type ?u.30876
R : Type u_1
m : Type ?u.30882
n : Type ?u.30885
p : Type ?u.30888
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ (1 + A 0 0) * (1 + A 1 1) - A 0 1 * A 1 0 = 1 + (A 0 0 * A 1 1 - A 0 1 * A 1 0) + (A 0 0 + A 1 1)

State before:
ι : Type ?u.30876
R : Type u_1
m : Type ?u.30882
n : Type ?u.30885
p : Type ?u.30888
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ (1 + A 0 0) * (1 + A 1 1) - A 0 1 * A 1 0 = 1 + (A 0 0 * A 1 1 - A 0 1 * A 1 0) + (A 0 0 + A 1 1)
Tactic:
ring
State after:
no goals