field_simp
ι : Type ?u.74781
R : Type u_1
m : Type ?u.74787
n : Type ?u.74790
p : Type ?u.74793
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 4) (Fin 4) R
inst✝ : CharZero R
⊢ (1 + A).det =
    1 + A.det + A.trace + 1 / 2 * (A.trace ^ 2 - (A ^ 2).trace) +
      1 / 6 * (A.trace ^ 3 - 3 * A.trace * (A ^ 2).trace + 2 * (A ^ 3).trace)
ι : Type ?u.74781
R : Type u_1
m : Type ?u.74787
n : Type ?u.74790
p : Type ?u.74793
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 4) (Fin 4) R
inst✝ : CharZero R
⊢ (1 + A).det * (2 * 6) =
    ((1 + A.det + A.trace) * 2 + (A.trace ^ 2 - (A ^ 2).trace)) * 6 +
      (A.trace ^ 3 - 3 * A.trace * (A ^ 2).trace + 2 * (A ^ 3).trace) * 2