ring
ι : 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 0 0 + (1 + A 0 0) * A 1 1) + 2 * ((1 + A 0 0 + (1 + A 0 0) * A 1 1) * A 2 2) -
              2 * ((1 + A 0 0) * A 1 2 * A 2 1) -
            (2 * (A 0 1 * A 1 0) + 2 * (A 0 1 * A 1 0 * A 2 2)) +
          2 * (A 0 1 * A 1 2 * A 2 0) +
        2 * (A 0 2 * A 1 0 * A 2 1) -
      2 * ((A 0 2 + A 0 2 * A 1 1) * A 2 0) =
    2 +
            (2 * (A 0 0 * A 1 1 * A 2 2) - 2 * (A 0 0 * A 1 2 * A 2 1) - 2 * (A 0 1 * A 1 0 * A 2 2) +
                  2 * (A 0 1 * A 1 2 * A 2 0) +
                2 * (A 0 2 * A 1 0 * A 2 1) -
              2 * (A 0 2 * A 1 1 * A 2 0)) +
          (2 * A 0 0 + 2 * A 1 1 + 2 * A 2 2) +
        ((A 0 0 + A 1 1 + A 2 2) * A 0 0 + (A 0 0 + A 1 1 + A 2 2) * A 1 1 + (A 0 0 + A 1 1 + A 2 2) * A 2 2) -
      (A 0 0 * A 0 0 + (A 0 1 * A 1 0 + A 0 2 * A 2 0) + (A 1 0 * A 0 1 + (A 1 1 * A 1 1 + A 1 2 * A 2 1)) +
        (A 2 0 * A 0 2 + (A 2 1 * A 1 2 + A 2 2 * A 2 2)))
no goals