apply mul_left_cancel₀ (isUnit_of_invertible (2 : R)).ne_zero
ι : Type ?u.45702
R : Type u_1
m : Type ?u.45708
n : Type ?u.45711
p : Type ?u.45714
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 3) (Fin 3) R
inst✝ : Invertible 2
⊢ (1 + A).det = 1 + A.det + A.trace + ⅟2 * A.trace ^ 2 - ⅟2 * (A ^ 2).trace
ι : Type ?u.45702
R : Type u_1
m : Type ?u.45708
n : Type ?u.45711
p : Type ?u.45714
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 3) (Fin 3) R
inst✝ : Invertible 2
⊢ 2 * (1 + A).det = 2 * (1 + A.det + A.trace + ⅟2 * A.trace ^ 2 - ⅟2 * (A ^ 2).trace)