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

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

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