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

State before:
ι : 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)
Tactic:
field_simp
State after:
ι : 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

State before:
ι : 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
Tactic:
rw [det_one_add_fin_four, det_fin_four, trace_pow_three_fin_four, trace_pow_two_fin_four,
  sq_trace_fin_four, trace_fin_four]
State after:
ι : 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
⊢ (A 0 0 + A 1 1 + A 2 2 + A 3 3 + A 0 0 * A 1 1 - A 0 1 * A 1 0 + A 0 0 * A 2 2 - A 0 2 * A 2 0 + A 0 0 * A 3 3 -
                                                                                                                      A
                                                                                                                          0
                                                                                                                          3 *
                                                                                                                        A
                                                                                                                          3
                                                                                                                          0 +
                                                                                                                    A 1
                                                                                                                        1 *
                                                                                                                      A
                                                                                                                        2
                                                                                                                        2 -
                                                                                                                  A 1
                                                                                                                      2 *
                                                                                                                    A 2
                                                                                                                      1 +
                                                                                                                A 1 1 *
                                                                                                                  A 3
                                                                                                                    3 -
                                                                                                              A 1 3 *
                                                                                                                A 3 1 +
                                                                                                            A 2 2 *
                                                                                                              A 3 3 -
                                                                                                          A 2 3 *
                                                                                                            A 3 2 +
                                                                                                        A 0 0 * A 1 1 *
                                                                                                          A 2 2 -
                                                                                                      A 0 0 * A 1 2 *
                                                                                                        A 2 1 -
                                                                                                    A 0 1 * A 1 0 *
                                                                                                      A 2 2 +
                                                                                                  A 0 1 * A 1 2 *
                                                                                                    A 2 0 +
                                                                                                A 0 2 * A 1 0 * A 2 1 -
                                                                                              A 0 2 * A 1 1 * A 2 0 +
                                                                                            A 0 0 * A 1 1 * A 3 3 -
                                                                                          A 0 0 * A 1 3 * A 3 1 -
                                                                                        A 0 1 * A 1 0 * A 3 3 +
                                                                                      A 0 1 * A 1 3 * A 3 0 +
                                                                                    A 0 3 * A 1 0 * A 3 1 -
                                                                                  A 0 3 * A 1 1 * A 3 0 +
                                                                                A 0 0 * A 2 2 * A 3 3 -
                                                                              A 0 0 * A 2 3 * A 3 2 -
                                                                            A 0 2 * A 2 0 * A 3 3 +
                                                                          A 0 2 * A 2 3 * A 3 0 +
                                                                        A 0 3 * A 2 0 * A 3 2 -
                                                                      A 0 3 * A 2 2 * A 3 0 +
                                                                    A 1 1 * A 2 2 * A 3 3 -
                                                                  A 1 1 * A 2 3 * A 3 2 -
                                                                A 1 2 * A 2 1 * A 3 3 +
                                                              A 1 2 * A 2 3 * A 3 1 +
                                                            A 1 3 * A 2 1 * A 3 2 -
                                                          A 1 3 * A 2 2 * A 3 1 +
                                                        A 0 0 * A 1 1 * A 2 2 * A 3 3 -
                                                      A 0 0 * A 1 1 * A 2 3 * A 3 2 -
                                                    A 0 0 * A 1 2 * A 2 1 * A 3 3 +
                                                  A 0 0 * A 1 2 * A 2 3 * A 3 1 +
                                                A 0 0 * A 1 3 * A 2 1 * A 3 2 -
                                              A 0 0 * A 1 3 * A 2 2 * A 3 1 -
                                            A 0 1 * A 1 0 * A 2 2 * A 3 3 +
                                          A 0 1 * A 1 0 * A 2 3 * A 3 2 +
                                        A 0 1 * A 1 2 * A 2 0 * A 3 3 -
                                      A 0 1 * A 1 2 * A 2 3 * A 3 0 -
                                    A 0 1 * A 1 3 * A 2 0 * A 3 2 +
                                  A 0 1 * A 1 3 * A 2 2 * A 3 0 +
                                A 0 2 * A 1 0 * A 2 1 * A 3 3 -
                              A 0 2 * A 1 0 * A 2 3 * A 3 1 -
                            A 0 2 * A 1 1 * A 2 0 * A 3 3 +
                          A 0 2 * A 1 1 * A 2 3 * A 3 0 +
                        A 0 2 * A 1 3 * A 2 0 * A 3 1 -
                      A 0 2 * A 1 3 * A 2 1 * A 3 0 -
                    A 0 3 * A 1 0 * A 2 1 * A 3 2 +
                  A 0 3 * A 1 0 * A 2 2 * A 3 1 +
                A 0 3 * A 1 1 * A 2 0 * A 3 2 -
              A 0 3 * A 1 1 * A 2 2 * A 3 0 -
            A 0 3 * A 1 2 * A 2 0 * A 3 1 +
          A 0 3 * A 1 2 * A 2 1 * A 3 0 +
        1) *
      (2 * 6) =
    ((1 +
                (A 0 0 * A 1 1 * A 2 2 * A 3 3 - A 0 0 * A 1 1 * A 2 3 * A 3 2 - A 0 0 * A 1 2 * A 2 1 * A 3 3 +
                                                          A 0 0 * A 1 2 * A 2 3 * A 3 1 +
                                                        A 0 0 * A 1 3 * A 2 1 * A 3 2 -
                                                      A 0 0 * A 1 3 * A 2 2 * A 3 1 -
                                                    A 0 1 * A 1 0 * A 2 2 * A 3 3 +
                                                  A 0 1 * A 1 0 * A 2 3 * A 3 2 +
                                                A 0 1 * A 1 2 * A 2 0 * A 3 3 -
                                              A 0 1 * A 1 2 * A 2 3 * A 3 0 -
                                            A 0 1 * A 1 3 * A 2 0 * A 3 2 +
                                          A 0 1 * A 1 3 * A 2 2 * A 3 0 +
                                        A 0 2 * A 1 0 * A 2 1 * A 3 3 -
                                      A 0 2 * A 1 0 * A 2 3 * A 3 1 -
                                    A 0 2 * A 1 1 * A 2 0 * A 3 3 +
                                  A 0 2 * A 1 1 * A 2 3 * A 3 0 +
                                A 0 2 * A 1 3 * A 2 0 * A 3 1 -
                              A 0 2 * A 1 3 * A 2 1 * A 3 0 -
                            A 0 3 * A 1 0 * A 2 1 * A 3 2 +
                          A 0 3 * A 1 0 * A 2 2 * A 3 1 +
                        A 0 3 * A 1 1 * A 2 0 * A 3 2 -
                      A 0 3 * A 1 1 * A 2 2 * A 3 0 -
                    A 0 3 * A 1 2 * A 2 0 * A 3 1 +
                  A 0 3 * A 1 2 * A 2 1 * A 3 0) +
              (A 0 0 + A 1 1 + A 2 2 + A 3 3)) *
            2 +
          (A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 0 * A 1 1 + 2 * A 0 0 * A 2 2 + 2 * A 0 0 * A 3 3 +
                  2 * A 1 1 * A 2 2 +
                2 * A 1 1 * A 3 3 +
              2 * A 2 2 * A 3 3 -
            (A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 1 * A 1 0 + 2 * A 0 2 * A 2 0 + 2 * A 0 3 * A 3 0 +
                  2 * A 1 2 * A 2 1 +
                2 * A 1 3 * A 3 1 +
              2 * A 2 3 * A 3 2))) *
        6 +
      ((A 0 0 + A 1 1 + A 2 2 + A 3 3) ^ 3 -
            3 * (A 0 0 + A 1 1 + A 2 2 + A 3 3) *
              (A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 1 * A 1 0 + 2 * A 0 2 * A 2 0 +
                      2 * A 0 3 * A 3 0 +
                    2 * A 1 2 * A 2 1 +
                  2 * A 1 3 * A 3 1 +
                2 * A 2 3 * A 3 2) +
          2 *
            (A 0 0 * (A 0 0 ^ 2 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0) +
                                          A 1 1 * (A 1 1 ^ 2 + A 0 1 * A 1 0 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
                                        A 2 2 * (A 2 2 ^ 2 + A 0 2 * A 2 0 + A 1 2 * A 2 1 + A 2 3 * A 3 2) +
                                      A 3 3 * (A 3 3 ^ 2 + A 0 3 * A 3 0 + A 1 3 * A 3 1 + A 2 3 * A 3 2) +
                                    A 1 0 * (A 0 0 * A 0 1 + A 0 1 * A 1 1 + A 0 2 * A 2 1 + A 0 3 * A 3 1) +
                                  A 2 0 * (A 0 0 * A 0 2 + A 0 1 * A 1 2 + A 0 2 * A 2 2 + A 0 3 * A 3 2) +
                                A 0 1 * (A 0 0 * A 1 0 + A 1 0 * A 1 1 + A 1 2 * A 2 0 + A 1 3 * A 3 0) +
                              A 3 0 * (A 0 0 * A 0 3 + A 0 1 * A 1 3 + A 0 2 * A 2 3 + A 0 3 * A 3 3) +
                            A 2 1 * (A 0 2 * A 1 0 + A 1 1 * A 1 2 + A 1 2 * A 2 2 + A 1 3 * A 3 2) +
                          A 0 2 * (A 0 0 * A 2 0 + A 1 0 * A 2 1 + A 2 0 * A 2 2 + A 2 3 * A 3 0) +
                        A 3 1 * (A 0 3 * A 1 0 + A 1 1 * A 1 3 + A 1 2 * A 2 3 + A 1 3 * A 3 3) +
                      A 1 2 * (A 0 1 * A 2 0 + A 1 1 * A 2 1 + A 2 1 * A 2 2 + A 2 3 * A 3 1) +
                    A 0 3 * (A 0 0 * A 3 0 + A 1 0 * A 3 1 + A 2 0 * A 3 2 + A 3 0 * A 3 3) +
                  A 3 2 * (A 0 3 * A 2 0 + A 1 3 * A 2 1 + A 2 2 * A 2 3 + A 2 3 * A 3 3) +
                A 1 3 * (A 0 1 * A 3 0 + A 1 1 * A 3 1 + A 2 1 * A 3 2 + A 3 1 * A 3 3) +
              A 2 3 * (A 0 2 * A 3 0 + A 1 2 * A 3 1 + A 2 2 * A 3 2 + A 3 2 * A 3 3))) *
        2

State before:
ι : 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
⊢ (A 0 0 + A 1 1 + A 2 2 + A 3 3 + A 0 0 * A 1 1 - A 0 1 * A 1 0 + A 0 0 * A 2 2 - A 0 2 * A 2 0 + A 0 0 * A 3 3 -
                                                                                                                      A
                                                                                                                          0
                                                                                                                          3 *
                                                                                                                        A
                                                                                                                          3
                                                                                                                          0 +
                                                                                                                    A 1
                                                                                                                        1 *
                                                                                                                      A
                                                                                                                        2
                                                                                                                        2 -
                                                                                                                  A 1
                                                                                                                      2 *
                                                                                                                    A 2
                                                                                                                      1 +
                                                                                                                A 1 1 *
                                                                                                                  A 3
                                                                                                                    3 -
                                                                                                              A 1 3 *
                                                                                                                A 3 1 +
                                                                                                            A 2 2 *
                                                                                                              A 3 3 -
                                                                                                          A 2 3 *
                                                                                                            A 3 2 +
                                                                                                        A 0 0 * A 1 1 *
                                                                                                          A 2 2 -
                                                                                                      A 0 0 * A 1 2 *
                                                                                                        A 2 1 -
                                                                                                    A 0 1 * A 1 0 *
                                                                                                      A 2 2 +
                                                                                                  A 0 1 * A 1 2 *
                                                                                                    A 2 0 +
                                                                                                A 0 2 * A 1 0 * A 2 1 -
                                                                                              A 0 2 * A 1 1 * A 2 0 +
                                                                                            A 0 0 * A 1 1 * A 3 3 -
                                                                                          A 0 0 * A 1 3 * A 3 1 -
                                                                                        A 0 1 * A 1 0 * A 3 3 +
                                                                                      A 0 1 * A 1 3 * A 3 0 +
                                                                                    A 0 3 * A 1 0 * A 3 1 -
                                                                                  A 0 3 * A 1 1 * A 3 0 +
                                                                                A 0 0 * A 2 2 * A 3 3 -
                                                                              A 0 0 * A 2 3 * A 3 2 -
                                                                            A 0 2 * A 2 0 * A 3 3 +
                                                                          A 0 2 * A 2 3 * A 3 0 +
                                                                        A 0 3 * A 2 0 * A 3 2 -
                                                                      A 0 3 * A 2 2 * A 3 0 +
                                                                    A 1 1 * A 2 2 * A 3 3 -
                                                                  A 1 1 * A 2 3 * A 3 2 -
                                                                A 1 2 * A 2 1 * A 3 3 +
                                                              A 1 2 * A 2 3 * A 3 1 +
                                                            A 1 3 * A 2 1 * A 3 2 -
                                                          A 1 3 * A 2 2 * A 3 1 +
                                                        A 0 0 * A 1 1 * A 2 2 * A 3 3 -
                                                      A 0 0 * A 1 1 * A 2 3 * A 3 2 -
                                                    A 0 0 * A 1 2 * A 2 1 * A 3 3 +
                                                  A 0 0 * A 1 2 * A 2 3 * A 3 1 +
                                                A 0 0 * A 1 3 * A 2 1 * A 3 2 -
                                              A 0 0 * A 1 3 * A 2 2 * A 3 1 -
                                            A 0 1 * A 1 0 * A 2 2 * A 3 3 +
                                          A 0 1 * A 1 0 * A 2 3 * A 3 2 +
                                        A 0 1 * A 1 2 * A 2 0 * A 3 3 -
                                      A 0 1 * A 1 2 * A 2 3 * A 3 0 -
                                    A 0 1 * A 1 3 * A 2 0 * A 3 2 +
                                  A 0 1 * A 1 3 * A 2 2 * A 3 0 +
                                A 0 2 * A 1 0 * A 2 1 * A 3 3 -
                              A 0 2 * A 1 0 * A 2 3 * A 3 1 -
                            A 0 2 * A 1 1 * A 2 0 * A 3 3 +
                          A 0 2 * A 1 1 * A 2 3 * A 3 0 +
                        A 0 2 * A 1 3 * A 2 0 * A 3 1 -
                      A 0 2 * A 1 3 * A 2 1 * A 3 0 -
                    A 0 3 * A 1 0 * A 2 1 * A 3 2 +
                  A 0 3 * A 1 0 * A 2 2 * A 3 1 +
                A 0 3 * A 1 1 * A 2 0 * A 3 2 -
              A 0 3 * A 1 1 * A 2 2 * A 3 0 -
            A 0 3 * A 1 2 * A 2 0 * A 3 1 +
          A 0 3 * A 1 2 * A 2 1 * A 3 0 +
        1) *
      (2 * 6) =
    ((1 +
                (A 0 0 * A 1 1 * A 2 2 * A 3 3 - A 0 0 * A 1 1 * A 2 3 * A 3 2 - A 0 0 * A 1 2 * A 2 1 * A 3 3 +
                                                          A 0 0 * A 1 2 * A 2 3 * A 3 1 +
                                                        A 0 0 * A 1 3 * A 2 1 * A 3 2 -
                                                      A 0 0 * A 1 3 * A 2 2 * A 3 1 -
                                                    A 0 1 * A 1 0 * A 2 2 * A 3 3 +
                                                  A 0 1 * A 1 0 * A 2 3 * A 3 2 +
                                                A 0 1 * A 1 2 * A 2 0 * A 3 3 -
                                              A 0 1 * A 1 2 * A 2 3 * A 3 0 -
                                            A 0 1 * A 1 3 * A 2 0 * A 3 2 +
                                          A 0 1 * A 1 3 * A 2 2 * A 3 0 +
                                        A 0 2 * A 1 0 * A 2 1 * A 3 3 -
                                      A 0 2 * A 1 0 * A 2 3 * A 3 1 -
                                    A 0 2 * A 1 1 * A 2 0 * A 3 3 +
                                  A 0 2 * A 1 1 * A 2 3 * A 3 0 +
                                A 0 2 * A 1 3 * A 2 0 * A 3 1 -
                              A 0 2 * A 1 3 * A 2 1 * A 3 0 -
                            A 0 3 * A 1 0 * A 2 1 * A 3 2 +
                          A 0 3 * A 1 0 * A 2 2 * A 3 1 +
                        A 0 3 * A 1 1 * A 2 0 * A 3 2 -
                      A 0 3 * A 1 1 * A 2 2 * A 3 0 -
                    A 0 3 * A 1 2 * A 2 0 * A 3 1 +
                  A 0 3 * A 1 2 * A 2 1 * A 3 0) +
              (A 0 0 + A 1 1 + A 2 2 + A 3 3)) *
            2 +
          (A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 0 * A 1 1 + 2 * A 0 0 * A 2 2 + 2 * A 0 0 * A 3 3 +
                  2 * A 1 1 * A 2 2 +
                2 * A 1 1 * A 3 3 +
              2 * A 2 2 * A 3 3 -
            (A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 1 * A 1 0 + 2 * A 0 2 * A 2 0 + 2 * A 0 3 * A 3 0 +
                  2 * A 1 2 * A 2 1 +
                2 * A 1 3 * A 3 1 +
              2 * A 2 3 * A 3 2))) *
        6 +
      ((A 0 0 + A 1 1 + A 2 2 + A 3 3) ^ 3 -
            3 * (A 0 0 + A 1 1 + A 2 2 + A 3 3) *
              (A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 1 * A 1 0 + 2 * A 0 2 * A 2 0 +
                      2 * A 0 3 * A 3 0 +
                    2 * A 1 2 * A 2 1 +
                  2 * A 1 3 * A 3 1 +
                2 * A 2 3 * A 3 2) +
          2 *
            (A 0 0 * (A 0 0 ^ 2 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0) +
                                          A 1 1 * (A 1 1 ^ 2 + A 0 1 * A 1 0 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
                                        A 2 2 * (A 2 2 ^ 2 + A 0 2 * A 2 0 + A 1 2 * A 2 1 + A 2 3 * A 3 2) +
                                      A 3 3 * (A 3 3 ^ 2 + A 0 3 * A 3 0 + A 1 3 * A 3 1 + A 2 3 * A 3 2) +
                                    A 1 0 * (A 0 0 * A 0 1 + A 0 1 * A 1 1 + A 0 2 * A 2 1 + A 0 3 * A 3 1) +
                                  A 2 0 * (A 0 0 * A 0 2 + A 0 1 * A 1 2 + A 0 2 * A 2 2 + A 0 3 * A 3 2) +
                                A 0 1 * (A 0 0 * A 1 0 + A 1 0 * A 1 1 + A 1 2 * A 2 0 + A 1 3 * A 3 0) +
                              A 3 0 * (A 0 0 * A 0 3 + A 0 1 * A 1 3 + A 0 2 * A 2 3 + A 0 3 * A 3 3) +
                            A 2 1 * (A 0 2 * A 1 0 + A 1 1 * A 1 2 + A 1 2 * A 2 2 + A 1 3 * A 3 2) +
                          A 0 2 * (A 0 0 * A 2 0 + A 1 0 * A 2 1 + A 2 0 * A 2 2 + A 2 3 * A 3 0) +
                        A 3 1 * (A 0 3 * A 1 0 + A 1 1 * A 1 3 + A 1 2 * A 2 3 + A 1 3 * A 3 3) +
                      A 1 2 * (A 0 1 * A 2 0 + A 1 1 * A 2 1 + A 2 1 * A 2 2 + A 2 3 * A 3 1) +
                    A 0 3 * (A 0 0 * A 3 0 + A 1 0 * A 3 1 + A 2 0 * A 3 2 + A 3 0 * A 3 3) +
                  A 3 2 * (A 0 3 * A 2 0 + A 1 3 * A 2 1 + A 2 2 * A 2 3 + A 2 3 * A 3 3) +
                A 1 3 * (A 0 1 * A 3 0 + A 1 1 * A 3 1 + A 2 1 * A 3 2 + A 3 1 * A 3 3) +
              A 2 3 * (A 0 2 * A 3 0 + A 1 2 * A 3 1 + A 2 2 * A 3 2 + A 3 2 * A 3 3))) *
        2
Tactic:
ring
State after:
no goals