Theorem: trace_pow_two_fin_four (MatrixCookbook/Lib/TraceDetFinFour.lean)

State before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ (A ^ 2).trace =
    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
Tactic:
simp_rw [Matrix.trace_fin_four, pow_two, mul_apply, Fin.sum_univ_four]
State after:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A 0 0 * A 0 0 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0 +
          (A 1 0 * A 0 1 + A 1 1 * A 1 1 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
        (A 2 0 * A 0 2 + A 2 1 * A 1 2 + A 2 2 * A 2 2 + A 2 3 * A 3 2) +
      (A 3 0 * A 0 3 + A 3 1 * A 1 3 + A 3 2 * A 2 3 + A 3 3 * A 3 3) =
    A 0 0 * A 0 0 + A 1 1 * A 1 1 + A 2 2 * A 2 2 + A 3 3 * A 3 3 + 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

State before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A 0 0 * A 0 0 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0 +
          (A 1 0 * A 0 1 + A 1 1 * A 1 1 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
        (A 2 0 * A 0 2 + A 2 1 * A 1 2 + A 2 2 * A 2 2 + A 2 3 * A 3 2) +
      (A 3 0 * A 0 3 + A 3 1 * A 1 3 + A 3 2 * A 2 3 + A 3 3 * A 3 3) =
    A 0 0 * A 0 0 + A 1 1 * A 1 1 + A 2 2 * A 2 2 + A 3 3 * A 3 3 + 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
Tactic:
ring
State after:
no goals