-- The Cayley–Hamilton theorem over a bundled commutative ring: the
-- characteristic polynomial charpoly(M) of a square matrix M, an element
-- of polynomialRing(R, {0}), evaluates at M to the zero matrix; the proof
-- reads the adjugate identity of the characteristic matrix inside the
-- commutant of M and contracts it against the columns of M; everything
-- here is ZF
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Ring.CayleyHamilton
import MatrixPolynomial
import Polynomial.Characteristic

notation function "charpoly(M)" => characteristicPolynomial(n, {0}, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), M, 0) via hypothesis Matrix(M, R, m, n)

-- The characteristic matrix M · 1 - M̃ of M over its commutant, M̃ the
-- matrix of scalar matrices, and its adjugate there.
def charMatrix (R n M : Set) : Set :=
  characteristicMatrix(n, Ring.carrier(commutant(R, n, M)),
    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
    Ring.one(commutant(R, n, M)),
    matrixMap(n, Ring.carrier(R), Ring.carrier(commutant(R, n, M)),
      scalarEmbedding(R, n), M), M)
def charAdjugate (R n M : Set) : Set :=
  adjugate(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),
    Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),
    Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)),
    charMatrix(R, n, M))

section Polynomials
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)

theorem charpoly.mem (M : R ^ n × n)
  shows charpoly(M) ∈ polynomialRing(R, {0})
proof
  have parts := CommRing.parts with comm
  have square := Matrix.square at M, R, n with assumption
  have shape := squareMatrices.membership.forward with square
  have index : 0 ∈ {0} by simp [singleton.membership]
  have member := characteristicPolynomial.member at {0}, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, n, M, 0 with *
  rw polynomialRing.carrierOf
  exact member

theorem charMatrix.scalars (M : R ^ n × n)
  shows RingMatrix(n, Ring.carrier(commutant(R, n, M)),
    matrixMap(n, Ring.carrier(R), Ring.carrier(commutant(R, n, M)), scalarEmbedding(R, n), M))
proof
  have target := commutant.comm_ring at R, n, M with *
  have hom := scalarEmbedding.hom at R, n, M with *
  have function : scalarEmbedding(R, n) : R.carrier → Ring.carrier(commutant(R, n, M))
    have parts := RingHom.parts with hom
    exact IsRingHom.function with parts
  have square := Matrix.square at M, R, n with assumption
  have shape := squareMatrices.membership.forward with square
  exact matrixMap.matrix with shape, function

theorem charMatrix.scalar_entry (M : R ^ n × n) (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows matrixMap(n, Ring.carrier(R), Ring.carrier(commutant(R, n, M)), scalarEmbedding(R, n), M)[i, j] =
    scalarMatrix(R, n, M[i, j])
proof
  have natural : Nat(n) by typecheck
  have target := commutant.comm_ring at R, n, M with *
  have hom := scalarEmbedding.hom at R, n, M with *
  have function : scalarEmbedding(R, n) : R.carrier → Ring.carrier(commutant(R, n, M))
    have parts := RingHom.parts with hom
    exact IsRingHom.function with parts
  have square := Matrix.square at M, R, n with assumption
  have shape := squareMatrices.membership.forward with square
  have entry := Matrix.entry at M, R, n, i, j with *
  have mapped := matrixMap.entry at n, R.carrier, Ring.carrier(commutant(R, n, M)),
    scalarEmbedding(R, n), M, i, j with *
  have value := scalarEmbedding.value at R, n, M[i, j] with *
  rw mapped
  exact value

theorem charMatrix.matrix (M : R ^ n × n)
  shows RingMatrix(n, Ring.carrier(commutant(R, n, M)), charMatrix(R, n, M))
proof
  have target := commutant.comm_ring at R, n, M with *
  have targetParts := CommRing.parts with target
  have scalars := charMatrix.scalars at R, n, M with *
  have self := commutant.self_mem at R, n, M with *
  unfold charMatrix
  exact characteristicMatrix.matrix with *

theorem charMatrix.entry (M : R ^ n × n) (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows charMatrix(R, n, M)[i, j] =
    call2(Ring.add(commutant(R, n, M)),
      singleValue(Ring.carrier(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), M, j, i),
      Ring.neg(commutant(R, n, M))(scalarMatrix(R, n, M[i, j])))
proof
  have target := commutant.comm_ring at R, n, M with *
  have targetParts := CommRing.parts with target
  have scalars := charMatrix.scalars at R, n, M with *
  have self := commutant.self_mem at R, n, M with *
  have entry := characteristicMatrix.entry at n, Ring.carrier(commutant(R, n, M)),
    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
    Ring.one(commutant(R, n, M)),
    matrixMap(n, Ring.carrier(R), Ring.carrier(commutant(R, n, M)), scalarEmbedding(R, n), M),
    M, i, j with *
  have scalar := charMatrix.scalar_entry at R, n, M, i, j with *
  unfold charMatrix
  cc

theorem charAdjugate.matrix (M : R ^ n × n)
  shows RingMatrix(n, Ring.carrier(commutant(R, n, M)), charAdjugate(R, n, M))
proof
  have target := commutant.comm_ring at R, n, M with *
  have targetParts := CommRing.parts with target
  have finite := Finite.natural at n
  have matrix := charMatrix.matrix at R, n, M with *
  unfold charAdjugate
  exact adjugate.matrix with *

end Polynomials

-- The entries of the terms of a finite sum in the commutant.
defgraph entryWeights (R n M V u a b : Set) (x ∈ V) : Ring.carrier(R) := u(x)[a, b]
requires comm : CommRing(R)
requires natural : Nat(n)
requires matrix : M : R ^ n × n
requires weights : u : V → Ring.carrier(commutant(R, n, M))
requires row : a ∈ n
requires column : b ∈ n
proof
  have value := FunctionBetween.apply_closed with weights, member
  have guard := commutant.mem_matrix with value
  exact Matrix.entry with guard, row, column

section Sums
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)

theorem indexedRingSum.commutant_entry (M : R ^ n × n) (V u f a b : Set, k : Nat)
  shows (∀ i ∈ k, f(i) ∈ V) → (u : V → Ring.carrier(commutant(R, n, M))) →
    a ∈ n → b ∈ n →
    indexedRingSum(u, f, Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), k)[a, b] =
      indexedRingSum(entryWeights(R, n, M, V, u, a, b), f, R.add, R.zero, k)
proof
  induction k
  | zero =>
    intros positions weights row column
    have zero := commutant.zero_value at R, n, M with *
    have entry := matrixRing.zero_entry at R, n, a, b with *
    rw [indexedRingSum, indexedRingSum, zero]
    exact entry
  | succ(m) using ih =>
    intros positions weights row column
    have natural : Nat(n) by typecheck
    have target := commutant.comm_ring at R, n, M with *
    have targetParts := CommRing.parts with target
    have smaller : ∀ i ∈ m, f(i) ∈ V
      intros i hi
      have next := membership.into_successor at i, m with *
      exact positions with i, next
    have previous := ih with smaller, weights, row, column
    have values : WeightedValues(u, f, Ring.carrier(commutant(R, n, M)), m)
      intros i hi
      have position := smaller with i, hi
      exact FunctionBetween.apply_closed with weights, position
    have closure := indexedRingSum.closed at Ring.carrier(commutant(R, n, M)),
      Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
      Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
      Ring.one(commutant(R, n, M)), u, f, m with *
    have prefixIn := closure with values
    have lastPosition := positions with m, membership.self_successor at m with *
    have lastIn := FunctionBetween.apply_closed with weights, lastPosition
    have prefixGuard := commutant.mem_matrix with prefixIn
    have lastGuard := commutant.mem_matrix with lastIn
    have sum := commutant.add_value at R, n, M,
      indexedRingSum(u, f, Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), m),
      u(f(m)) with *
    have entry := matrixRing.add_entry at R, n,
      indexedRingSum(u, f, Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), m),
      u(f(m)), a, b with *
    have graph := entryWeights.function at R, n, M, V, u, a, b with *
    have weight := entryWeights.value at R, n, M, V, u, a, b, f(m) with *
    rw [indexedRingSum, indexedRingSum, sum, entry, previous, weight]
    rfl

theorem finiteRingSum.commutant_entry (M : R ^ n × n) (V u a b : Set)
  requires finite : Finite(V)
  requires weights : u : V → Ring.carrier(commutant(R, n, M))
  requires row : a ∈ n
  requires column : b ∈ n
  shows finiteRingSum(V, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),
      Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),
      Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), u)[a, b] =
    finiteRingSum(V, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,
      entryWeights(R, n, M, V, u, a, b))
proof
  have natural : Nat(n) by typecheck
  have parts := CommRing.parts with comm
  have target := commutant.comm_ring at R, n, M with *
  have targetParts := CommRing.parts with target
  have graph := entryWeights.function at R, n, M, V, u, a, b with *
  have selected := finiteRingSum.selected at V, Ring.carrier(commutant(R, n, M)),
    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
    Ring.one(commutant(R, n, M)), u with *
  obtain ⟨m, naturalM, f, enumeration, equationS⟩ := selected.right
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have equationR := finiteRingSum.enumeration at V, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, entryWeights(R, n, M, V, u, a, b), f, m with *
  have positions : ∀ i ∈ m, f(i) ∈ V
    intros i hi
    exact FunctionBetween.apply_closed with function, hi
  have step := indexedRingSum.commutant_entry at R, n, M, V, u, f, a, b, m with *
  rw [equationS, equationR]
  exact step with positions, weights, row, column

end Sums

-- The entries (i, i) of the column j of the characteristic matrix, as
-- matrices, read at row e: the annihilation relation says they sum to 0.
defgraph kernelWeights (R n M j e : Set) (i ∈ n) : Ring.carrier(R) :=
  charMatrix(R, n, M)[i, j][e, i]
requires comm : CommRing(R)
requires natural : Nat(n)
requires matrix : M : R ^ n × n
requires column : j ∈ n
requires row : e ∈ n
proof
  have shape := charMatrix.matrix at R, n, M with *
  have entry := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),
    charMatrix(R, n, M), i, j with *
  have guard := commutant.mem_matrix with entry
  exact Matrix.entry with guard, row, member

section Kernel
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)

theorem charMatrix.column_sum (M : R ^ n × n) (j e : Set)
  requires column : j ∈ n
  requires row : e ∈ n
  shows finiteRingSum(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,
    kernelWeights(R, n, M, j, e)) = R[0]
proof
  have natural : Nat(n) by typecheck
  have parts := CommRing.parts with comm
  have finite := Finite.natural at n
  have ringT := matrixRing.ring at R, n with *
  have partsT := Ring.parts with ringT
  have target := commutant.comm_ring at R, n, M with *
  have targetParts := CommRing.parts with target
  have targetRing := IsCommRing.ring with targetParts
  have self := commutant.self_mem at R, n, M with *
  have zeroS := commutant.zero_value at R, n, M with *
  have zeroIn : R[0] ∈ R := Ring.zero_mem with *
  have oneIn : R[1] ∈ R := Ring.one_mem with *
  have minusOne : R[-1] ∈ R := Ring.neg_mem with *
  have entryEJ := Matrix.entry at M, R, n, e, j with *
  have weights := kernelWeights.function at R, n, M, j, e with *
  have firstSel := coefficientSingle.function at n, R.carrier, R.zero, M[e, j], j with *
  have secondSel := coefficientSingle.function at n, R.carrier, R.zero, M[e, j], e with *
  have values : ∀ i ∈ n, kernelWeights(R, n, M, j, e)(i) =
      R[1] * coefficientSingle(n, Ring.carrier(R), R.zero, M[e, j], j)(i) +
        R[-1] * coefficientSingle(n, Ring.carrier(R), R.zero, M[e, j], e)(i)
    intros i hi
    have entryIJ := Matrix.entry at M, R, n, i, j with *
    have weight := kernelWeights.value at R, n, M, j, e, i with *
    have entry := charMatrix.entry at R, n, M, i, j with *
    have deltaIn := singleValue.closed at Ring.carrier(commutant(R, n, M)),
      Ring.zero(commutant(R, n, M)), M, j, i with *
    have scalarIn := commutant.scalar_mem at R, n, M, M[i, j] with *
    have negIn := IsRing.neg_closed with targetRing, scalarIn
    have sum := commutant.add_value at R, n, M,
      singleValue(Ring.carrier(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), M, j, i),
      Ring.neg(commutant(R, n, M))(scalarMatrix(R, n, M[i, j])) with *
    have negation := commutant.neg_value at R, n, M, scalarMatrix(R, n, M[i, j]) with *
    have deltaGuard := commutant.mem_matrix with deltaIn
    have scalarGuard := scalarMatrix.guard at R, n, M[i, j] with *
    have scalarMem := Matrix.mem_ring with scalarGuard
    have negMem := IsRing.neg_closed with partsT, scalarMem
    have negGuard := Matrix.of_mem with negMem
    have addEntry := matrixRing.add_entry at R, n,
      singleValue(Ring.carrier(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), M, j, i),
      Ring.neg(matrixRing(R, n))(scalarMatrix(R, n, M[i, j])), e, i with *
    have negEntry := matrixRing.neg_entry at R, n, scalarMatrix(R, n, M[i, j]), e, i with *
    have scalarEntry := scalarMatrix.entry at R, n, M[i, j], e, i with *
    rw [weight, entry, sum, negation, addEntry, negEntry, scalarEntry]
    have alternatives : i = j ∨ i ≠ j by tauto
    cases alternatives with same | different
    . have delta := singleValue.same at Ring.carrier(commutant(R, n, M)),
        Ring.zero(commutant(R, n, M)), M, j, i with *
      have first := coefficientSingle.same at n, R.carrier, R.zero, M[e, j], j with *
      rw [delta, same, first]
      have entryJJ := Matrix.entry at M, R, n, j, j with *
      have alternativesE : e = j ∨ e ≠ j by tauto
      cases alternativesE with sameE | differentE
      . rw sameE
        have reflJ : j = j by rfl
        have unit := singleValue.same at R.carrier, R.zero, R.one, j, j with *
        have second := coefficientSingle.same at n, R.carrier, R.zero, M[j, j], j with *
        rw [unit, second]
        ring
      . have reverse : j ≠ e
          intro equal
          apply differentE
          cc
        have unit := singleValue.other at R.carrier, R.zero, R.one, j, e with *
        have second := coefficientSingle.other at n, R.carrier, R.zero, M[e, j], e, j with *
        rw [unit, second]
        ring
    . have delta := singleValue.other at Ring.carrier(commutant(R, n, M)),
        Ring.zero(commutant(R, n, M)), M, j, i with *
      have zeroEntry := matrixRing.zero_entry at R, n, e, i with *
      have first := coefficientSingle.other at n, R.carrier, R.zero, M[e, j], j, i with *
      rw [delta, zeroS, zeroEntry, first]
      have alternativesE : e = i ∨ e ≠ i by tauto
      cases alternativesE with sameE | differentE
      . rw sameE
        have reflI : i = i by rfl
        have unit := singleValue.same at R.carrier, R.zero, R.one, i, i with *
        have second := coefficientSingle.same at n, R.carrier, R.zero, M[i, j], i with *
        rw [unit, second]
        ring
      . have reverse : i ≠ e
          intro equal
          apply differentE
          cc
        have unit := singleValue.other at R.carrier, R.zero, R.one, i, e with *
        have second := coefficientSingle.other at n, R.carrier, R.zero, M[e, j], e, i with *
        rw [unit, second]
        ring
  have linear := finiteRingSum.linear at n, R.carrier, R.add, R.zero, R.neg, R.mul,
    R.one, coefficientSingle(n, R.carrier, R.zero, M[e, j], j),
    coefficientSingle(n, R.carrier, R.zero, M[e, j], e),
    kernelWeights(R, n, M, j, e), R[1], R[-1] with *
  have first := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg, R.mul,
    R.one, M[e, j], j with *
  have second := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg, R.mul,
    R.one, M[e, j], e with *
  rw [linear, first, second]
  ring

end Kernel

-- Contracting a matrix A against a family Q of matrices: the row sums of
-- the products A · Q(i) at the diagonal positions vanish when every
-- column family of Q sums to zero.
defgraph columnWeights (R n Q e : Set) (i ∈ n) : Ring.carrier(R) := Q(i)[e, i]
requires comm : CommRing(R)
requires family : Q : n → Ring.carrier(matrixRing(R, n))
requires row : e ∈ n
proof
  have value := FunctionBetween.apply_closed with family, member
  have guard := Matrix.of_mem with value
  exact Matrix.entry with guard, row, member

defgraph productWeights (R n A Q a : Set) (i ∈ n) : Ring.carrier(R) :=
  call2(Ring.mul(matrixRing(R, n)), A, Q(i))[a, i]
requires comm : CommRing(R)
requires natural : Nat(n)
requires matrix : A : R ^ n × n
requires family : Q : n → Ring.carrier(matrixRing(R, n))
requires row : a ∈ n
proof
  have ringT := matrixRing.ring at R, n with *
  have value := FunctionBetween.apply_closed with family, member
  have left := Matrix.mem_ring with matrix
  have partsT := Ring.parts with ringT
  have product := IsRing.mul_closed with partsT, left, value
  have guard := Matrix.of_mem with product
  exact Matrix.entry with guard, row, member

defunique contractionWeightValue (R : Set, n : Nat, A Q a q : Set) (x ∈ Ring.carrier(R)) :=
  ∃ i ∈ n, ∃ e ∈ n, q = (i, e) ∧ x = call2(Ring.mul(R), A[a, e], Q(i)[e, i])
requires comm : CommRing(R)
requires matrix : A : R ^ n × n
requires family : Q : n → Ring.carrier(matrixRing(R, n))
requires row : a ∈ n
requires pair : q ∈ n × n
proof
  obtain ⟨bound, i, hi, e, he, shape⟩ := product.membership.forward at
    n, n, q with *
  have parts := CommRing.parts with comm
  have ordinary := IsCommRing.ring with parts
  have entryA := Matrix.entry at A, R, n, a, e with *
  have value := FunctionBetween.apply_closed with family, hi
  have guard := Matrix.of_mem with value
  have entryQ := Matrix.entry at Q(i), R, n, e, i with *
  have product := IsRing.mul_closed with ordinary, entryA, entryQ
  refine ⟨call2(Ring.mul(R), A[a, e], Q(i)[e, i]), product, i, hi, e, he, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨i, hi, e, he, shapeU, valueU⟩ := first
  obtain ⟨k, hk, l, hl, shapeV, valueV⟩ := second
  have equal : (i, e) = (k, l)
    cc
  have coordinates := orderedPair.injective at i, e, k, l with equal
  cc

defgraph contractionWeights (R : Set, n : Nat, A Q a : Set) (q ∈ n × n) : Ring.carrier(R) :=
  contractionWeightValue(R, n, A, Q, a, q)
requires comm : CommRing(R)
requires matrix : A : R ^ n × n
requires family : Q : n → Ring.carrier(matrixRing(R, n))
requires row : a ∈ n
proof
  have selected := contractionWeightValue.selected at R, n, A, Q, a, q with *
  exact selected.left

theorem contractionWeights.pair (R : Set, n : Nat, A Q a i e : Set)
  requires comm : CommRing(R)
  requires matrix : A : R ^ n × n
  requires family : Q : n → Ring.carrier(matrixRing(R, n))
  requires row : a ∈ n
  requires hi : i ∈ n
  requires he : e ∈ n
  shows contractionWeights(R, n, A, Q, a)((i, e)) = A[a, e] * Q(i)[e, i]
proof
  have pair := product.pair at i, e, n, n with *
  have selected := contractionWeightValue.selected at R, n, A, Q, a, (i, e) with *
  obtain ⟨k, hk, l, hl, shape, result⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := contractionWeights.value at R, n, A, Q, a, (i, e) with *
  cc

section Contraction
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)

theorem Matrix.contraction_zero (A : R ^ n × n) (Q a : Set)
  requires family : Q : n → Ring.carrier(matrixRing(R, n))
  requires row : a ∈ n
  requires vanishing : ∀ e ∈ n, finiteRingSum(n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, columnWeights(R, n, Q, e)) = R[0]
  shows finiteRingSum(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,
    productWeights(R, n, A, Q, a)) = R[0]
proof
  have natural : Nat(n) by typecheck
  have parts := CommRing.parts with comm
  have finite := Finite.natural at n
  have ringT := matrixRing.ring at R, n with *
  have squareA := Matrix.square at A, R, n with assumption
  have shapeA := squareMatrices.membership.forward with squareA
  have array := contractionWeights.function at R, n, A, Q, a with *
  have transposed := transposedMatrix.function at n, n, R.carrier,
    contractionWeights(R, n, A, Q, a) with *
  have rowsL := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, contractionWeights(R, n, A, Q, a) with *
  have rowsR := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)) with *
  have products := productWeights.function at R, n, A, Q, a with *
  have leftRows : ∀ i ∈ n, productWeights(R, n, A, Q, a)(i) =
      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, contractionWeights(R, n, A, Q, a))(i)
    intros i hi
    have value := FunctionBetween.apply_closed with family, hi
    have guard := Matrix.of_mem with value
    have squareQ := Matrix.square with guard
    have shapeQ := squareMatrices.membership.forward with squareQ
    have weight := productWeights.value at R, n, A, Q, a, i with *
    have entry := matrixRing.mul_entry at R, n, A, Q(i), a, i with *
    have rowWeights := finiteRowWeights.function at n, n, R.carrier,
      contractionWeights(R, n, A, Q, a), i with *
    have inner := matrixProductWeights.function at n, R.carrier, R.add, R.zero,
      R.neg, R.mul, R.one, A, Q(i), a, i with *
    have cells : ∀ e ∈ n, matrixProductWeights(n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, A, Q(i), a, i)(e) =
        finiteRowWeights(n, n, Ring.carrier(R), contractionWeights(R, n, A, Q, a), i)(e)
      intros e he
      have product := matrixProductWeights.value at n, R.carrier, R.add, R.zero,
        R.neg, R.mul, R.one, A, Q(i), a, i, e with *
      have rowWeight := finiteRowWeights.value at n, n, R.carrier,
        contractionWeights(R, n, A, Q, a), i, e with *
      have cell := contractionWeights.pair at R, n, A, Q, a, i, e with *
      cc
    have same := finiteRingSum.congr with cells
    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, contractionWeights(R, n, A, Q, a), i with *
    unfold matrixProductEntry at entry
    cc
  have rightRows : ∀ e ∈ n,
      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, transposedMatrix(n, n, Ring.carrier(R), contractionWeights(R, n, A, Q, a)))(e) = R[0]
    intros e he
    have entryA := Matrix.entry at A, R, n, a, e with *
    have rowWeights := finiteRowWeights.function at n, n, R.carrier,
      transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)), e with *
    have columns := columnWeights.function at R, n, Q, e with *
    have scaled : ∀ i ∈ n, finiteRowWeights(n, n, Ring.carrier(R), transposedMatrix(n, n, Ring.carrier(R), contractionWeights(R, n, A, Q, a)), e)(i) =
        A[a, e] * columnWeights(R, n, Q, e)(i)
      intros i hi
      have rowWeight := finiteRowWeights.value at n, n, R.carrier,
        transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)), e, i with *
      have swap := transposedMatrix.pair at n, n, R.carrier,
        contractionWeights(R, n, A, Q, a), i, e with *
      have cell := contractionWeights.pair at R, n, A, Q, a, i, e with *
      have column := columnWeights.value at R, n, Q, e, i with *
      cc
    have scale := finiteRingSum.scale_eq at n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, columnWeights(R, n, Q, e),
      finiteRowWeights(n, n, R.carrier, transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)), e),
      A[a, e] with *
    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)), e with *
    have vanish := vanishing with e, he
    rw [rowSum, scale, vanish]
    ring
  have sameL := finiteRingSum.congr with leftRows
  have sumR := finiteRingSum.zero with rightRows
  have interchange := finiteDoubleSum.interchange at n, n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, contractionWeights(R, n, A, Q, a) with *
  unfold finiteDoubleSum at interchange
  cc

end Contraction

-- The column j of the characteristic matrix as a family of matrices, the
-- diagonal entries of the adjugate identity read at row a, and the
-- products adj(j, k) · C(i, j) read at (a, i), as an array over n × n.
defgraph charColumn (R n M j : Set) (i ∈ n) : Ring.carrier(matrixRing(R, n)) :=
  charMatrix(R, n, M)[i, j]
requires comm : CommRing(R)
requires natural : Nat(n)
requires matrix : M : R ^ n × n
requires column : j ∈ n
proof
  have shape := charMatrix.matrix at R, n, M with *
  have entry := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),
    charMatrix(R, n, M), i, j with *
  have subset := commutant.subset at R, n, M with *
  exact subset with charMatrix(R, n, M)[i, j], entry

defgraph diagonalWeights (R n M k a : Set) (i ∈ n) : Ring.carrier(R) :=
  matrixProductEntry(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),
    Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),
    Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)),
    charMatrix(R, n, M), charAdjugate(R, n, M), i, k)[a, i]
requires comm : CommRing(R)
requires natural : Nat(n)
requires matrix : M : R ^ n × n
requires column : k ∈ n
requires row : a ∈ n
proof
  have target := commutant.comm_ring at R, n, M with *
  have targetParts := CommRing.parts with target
  have finite := Finite.natural at n
  have shapeC := charMatrix.matrix at R, n, M with *
  have shapeA := charAdjugate.matrix at R, n, M with *
  have weights := matrixProductWeights.function at n, Ring.carrier(commutant(R, n, M)),
    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
    Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k with *
  have closed : matrixProductEntry(n, Ring.carrier(commutant(R, n, M)),
      Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
      Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
      Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M),
      i, k) ∈ Ring.carrier(commutant(R, n, M))
    unfold matrixProductEntry
    exact finiteRingSum.closed with *
  have guard := commutant.mem_matrix with closed
  exact Matrix.entry with guard, row, member

defunique pairingWeightValue (R : Set, n : Nat, M k a q : Set) (x ∈ Ring.carrier(R)) :=
  ∃ i ∈ n, ∃ j ∈ n, q = (i, j) ∧
    x = call2(Ring.mul(matrixRing(R, n)), charAdjugate(R, n, M)[j, k], charMatrix(R, n, M)[i, j])[a, i]
requires comm : CommRing(R)
requires matrix : M : R ^ n × n
requires column : k ∈ n
requires row : a ∈ n
requires pair : q ∈ n × n
proof
  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward at
    n, n, q with *
  have ringT := matrixRing.ring at R, n with *
  have partsT := Ring.parts with ringT
  have shapeC := charMatrix.matrix at R, n, M with *
  have shapeA := charAdjugate.matrix at R, n, M with *
  have subset := commutant.subset at R, n, M with *
  have entryC := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),
    charMatrix(R, n, M), i, j with *
  have entryA := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),
    charAdjugate(R, n, M), j, k with *
  have leftIn := subset with charAdjugate(R, n, M)[j, k], entryA
  have rightIn := subset with charMatrix(R, n, M)[i, j], entryC
  have product := IsRing.mul_closed with partsT, leftIn, rightIn
  have guard := Matrix.of_mem with product
  have value := Matrix.entry at call2(Ring.mul(matrixRing(R, n)), charAdjugate(R, n, M)[j, k], charMatrix(R, n, M)[i, j]), R, n, a, i with *
  refine ⟨call2(Ring.mul(matrixRing(R, n)), charAdjugate(R, n, M)[j, k], charMatrix(R, n, M)[i, j])[a, i], value, i, hi, j, hj, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨i, hi, j, hj, shapeU, valueU⟩ := first
  obtain ⟨p, hp, s, hs, shapeV, valueV⟩ := second
  have equal : (i, j) = (p, s)
    cc
  have coordinates := orderedPair.injective at i, j, p, s with equal
  cc

defgraph pairingWeights (R : Set, n : Nat, M k a : Set) (q ∈ n × n) : Ring.carrier(R) :=
  pairingWeightValue(R, n, M, k, a, q)
requires comm : CommRing(R)
requires matrix : M : R ^ n × n
requires column : k ∈ n
requires row : a ∈ n
proof
  have selected := pairingWeightValue.selected at R, n, M, k, a, q with *
  exact selected.left

theorem pairingWeights.pair (R : Set, n : Nat, M k a i j : Set)
  requires comm : CommRing(R)
  requires matrix : M : R ^ n × n
  requires column : k ∈ n
  requires row : a ∈ n
  requires hi : i ∈ n
  requires hj : j ∈ n
  shows pairingWeights(R, n, M, k, a)((i, j)) =
    call2(Ring.mul(matrixRing(R, n)), charAdjugate(R, n, M)[j, k], charMatrix(R, n, M)[i, j])[a, i]
proof
  have pair := product.pair at i, j, n, n with *
  have selected := pairingWeightValue.selected at R, n, M, k, a, (i, j) with *
  obtain ⟨p, hp, s, hs, shape, result⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := pairingWeights.value at R, n, M, k, a, (i, j) with *
  cc

section CayleyHamilton
variable (R : Set) (n : Nat)
hypothesis comm : CommRing(R)

-- The evaluation of the characteristic polynomial at M is the determinant
-- of the characteristic matrix over the commutant of M.
theorem charpoly.evaluate (M : R ^ n × n)
  shows evalAt(M)(charpoly(M)) = determinant(n, Ring.carrier(commutant(R, n, M)),
    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
    Ring.one(commutant(R, n, M)), charMatrix(R, n, M))
proof
  have parts := CommRing.parts with comm
  have target := commutant.comm_ring at R, n, M with *
  have targetParts := CommRing.parts with target
  have hom := scalarEmbedding.hom at R, n, M with *
  have homParts := RingHom.parts with hom
  have self := commutant.self_mem at R, n, M with *
  have assignment := constantFunction.function at {0}, Ring.carrier(commutant(R, n, M)), M with *
  have index : 0 ∈ {0} by simp [singleton.membership]
  have point := constantFunction.apply at {0}, Ring.carrier(commutant(R, n, M)), 0, M with *
  have square := Matrix.square at M, R, n with assumption
  have shape := squareMatrices.membership.forward with square
  have mapped := characteristicPolynomial.evaluate_mapped at {0}, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),
    Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),
    Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), scalarEmbedding(R, n),
    constantFunction({0}, Ring.carrier(commutant(R, n, M)), M), n, M, 0 with *
  rw point at mapped
  unfold matrixEvaluation
  rw evaluationHom.graph
  unfold charMatrix
  cc

-- The Cayley–Hamilton theorem: a square matrix satisfies its own
-- characteristic polynomial.
theorem Matrix.cayley_hamilton (M : R ^ n × n)
  shows evalAt(M)(charpoly(M)) = matrixRing(R, n)[0]
proof
  have natural : Nat(n) by typecheck
  have parts := CommRing.parts with comm
  have finite := Finite.natural at n
  have ringT := matrixRing.ring at R, n with *
  have partsT := Ring.parts with ringT
  have target := commutant.comm_ring at R, n, M with *
  have targetParts := CommRing.parts with target
  have subset := commutant.subset at R, n, M with *
  have shapeC := charMatrix.matrix at R, n, M with *
  have shapeA := charAdjugate.matrix at R, n, M with *
  have evaluated := charpoly.evaluate at R, n, M with *
  have determinantIn := determinant.closed at Ring.carrier(commutant(R, n, M)),
    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
    Ring.one(commutant(R, n, M)), charMatrix(R, n, M), n with *
  have determinantGuard := commutant.mem_matrix with determinantIn
  have zeroGuard := Matrix.of_mem at matrixRing(R, n)[0], R, n with (Ring.zero_mem with *)
  rw evaluated
  apply Matrix.ext with determinantGuard, zeroGuard
  intros a ha k hk
  have zeroEntry := matrixRing.zero_entry at R, n, a, k with *
  rw zeroEntry
  have determinantEntry := Matrix.entry at determinant(n, Ring.carrier(commutant(R, n, M)),
    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
    Ring.one(commutant(R, n, M)), charMatrix(R, n, M)), R, n, a, k with *
  have diagonals := diagonalWeights.function at R, n, M, k, a with *
  have selector := coefficientSingle.function at n, R.carrier, R.zero,
    determinant(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),
      Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),
      Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M))[a, k], k with *
  have array := pairingWeights.function at R, n, M, k, a with *
  have transposed := transposedMatrix.function at n, n, R.carrier,
    pairingWeights(R, n, M, k, a) with *
  have rowsL := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, pairingWeights(R, n, M, k, a) with *
  have rowsR := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, transposedMatrix(n, n, R.carrier, pairingWeights(R, n, M, k, a)) with *
  -- The adjugate identity in the commutant, entry by entry at row a.
  have diagonal : ∀ i ∈ n, diagonalWeights(R, n, M, k, a)(i) =
      coefficientSingle(n, Ring.carrier(R), R.zero, determinant(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M))[a, k], k)(i)
    intros i hi
    have weight := diagonalWeights.value at R, n, M, k, a, i with *
    have identity := adjugate.right_identity at Ring.carrier(commutant(R, n, M)),
      Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
      Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
      Ring.one(commutant(R, n, M)), n, charMatrix(R, n, M), i, k with *
    have unfolded : charAdjugate(R, n, M) = adjugate(n, Ring.carrier(commutant(R, n, M)),
        Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
        Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
        Ring.one(commutant(R, n, M)), charMatrix(R, n, M))
      simp [charAdjugate]
    rw [weight, unfolded, identity]
    have zeroIn := IsRing.zero_in_carrier with (IsCommRing.ring with targetParts)
    have alternatives : i = k ∨ i ≠ k by tauto
    cases alternatives with same | different
    . have delta := singleValue.same at Ring.carrier(commutant(R, n, M)),
        Ring.zero(commutant(R, n, M)), determinant(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M)), k, i with *
      have selected := coefficientSingle.same at n, R.carrier, R.zero,
        determinant(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M))[a, k], k with *
      rw [delta, same, selected]
      rfl
    . have delta := singleValue.other at Ring.carrier(commutant(R, n, M)),
        Ring.zero(commutant(R, n, M)), determinant(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M)), k, i with *
      have selected := coefficientSingle.other at n, R.carrier, R.zero,
        determinant(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M))[a, k], k, i with *
      have zeroEntryI := matrixRing.zero_entry at R, n, a, i with *
      have zeroS := commutant.zero_value at R, n, M with *
      have zeroEntryS : Ring.zero(commutant(R, n, M))[a, i] = R[0]
        rw zeroS
        exact zeroEntryI
      rw [delta, zeroEntryS, selected]
      rfl
  have sameDiagonal := finiteRingSum.congr with diagonal
  have single := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg, R.mul,
    R.one, determinant(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M))[a, k], k with *
  -- The same entries as the row sums of the pairing array.
  have rows : ∀ i ∈ n, diagonalWeights(R, n, M, k, a)(i) =
      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, pairingWeights(R, n, M, k, a))(i)
    intros i hi
    have weight := diagonalWeights.value at R, n, M, k, a, i with *
    have products := matrixProductWeights.function at n, Ring.carrier(commutant(R, n, M)),
      Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
      Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
      Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k with *
    have entries := finiteRingSum.commutant_entry at R, n, M, n,
      matrixProductWeights(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k),
      a, i with *
    have graph := entryWeights.function at R, n, M, n,
      matrixProductWeights(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k),
      a, i with *
    have rowWeights := finiteRowWeights.function at n, n, R.carrier,
      pairingWeights(R, n, M, k, a), i with *
    have cells : ∀ j ∈ n, entryWeights(R, n, M, n, matrixProductWeights(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k), a, i)(j) =
        finiteRowWeights(n, n, Ring.carrier(R), pairingWeights(R, n, M, k, a), i)(j)
      intros j hj
      have value := entryWeights.value at R, n, M, n,
        matrixProductWeights(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k),
        a, i, j with *
      have product := matrixProductWeights.value at n, Ring.carrier(commutant(R, n, M)),
        Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
        Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
        Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k, j with *
      have entryC := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),
        charMatrix(R, n, M), i, j with *
      have entryA := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),
        charAdjugate(R, n, M), j, k with *
      have swap := IsCommRing.mul_comm at Ring.carrier(commutant(R, n, M)),
        Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
        Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
        Ring.one(commutant(R, n, M)), charMatrix(R, n, M)[i, j], charAdjugate(R, n, M)[j, k] with *
      have lifted := commutant.mul_value at R, n, M, charAdjugate(R, n, M)[j, k],
        charMatrix(R, n, M)[i, j] with *
      have rowWeight := finiteRowWeights.value at n, n, R.carrier,
        pairingWeights(R, n, M, k, a), i, j with *
      have cell := pairingWeights.pair at R, n, M, k, a, i, j with *
      cc
    have same := finiteRingSum.congr with cells
    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, pairingWeights(R, n, M, k, a), i with *
    unfold matrixProductEntry at weight
    cc
  have sameRows := finiteRingSum.congr with rows
  -- Each column sum of the transposed array vanishes by the contraction.
  have columns : ∀ j ∈ n,
      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, transposedMatrix(n, n, Ring.carrier(R), pairingWeights(R, n, M, k, a)))(j) = R[0]
    intros j hj
    have entryA := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),
      charAdjugate(R, n, M), j, k with *
    have leftIn := subset with charAdjugate(R, n, M)[j, k], entryA
    have leftGuard := Matrix.of_mem with leftIn
    have family := charColumn.function at R, n, M, j with *
    have productsQ := productWeights.function at R, n, charAdjugate(R, n, M)[j, k],
      charColumn(R, n, M, j), a with *
    have rowWeights := finiteRowWeights.function at n, n, R.carrier,
      transposedMatrix(n, n, R.carrier, pairingWeights(R, n, M, k, a)), j with *
    have cells : ∀ i ∈ n, finiteRowWeights(n, n, Ring.carrier(R), transposedMatrix(n, n, Ring.carrier(R), pairingWeights(R, n, M, k, a)), j)(i) =
        productWeights(R, n, charAdjugate(R, n, M)[j, k], charColumn(R, n, M, j), a)(i)
      intros i hi
      have rowWeight := finiteRowWeights.value at n, n, R.carrier,
        transposedMatrix(n, n, R.carrier, pairingWeights(R, n, M, k, a)), j, i with *
      have swap := transposedMatrix.pair at n, n, R.carrier,
        pairingWeights(R, n, M, k, a), i, j with *
      have cell := pairingWeights.pair at R, n, M, k, a, i, j with *
      have columnValue := charColumn.value at R, n, M, j, i with *
      have productValue := productWeights.value at R, n, charAdjugate(R, n, M)[j, k],
        charColumn(R, n, M, j), a, i with *
      cc
    have same := finiteRingSum.congr with cells
    have vanishing : ∀ e ∈ n, finiteRingSum(n, R.carrier, R.add, R.zero, R.neg, R.mul,
        R.one, columnWeights(R, n, charColumn(R, n, M, j), e)) = R[0]
      intros e he
      have columnsQ := columnWeights.function at R, n, charColumn(R, n, M, j), e with *
      have kernel := kernelWeights.function at R, n, M, j, e with *
      have agree : ∀ i ∈ n, columnWeights(R, n, charColumn(R, n, M, j), e)(i) =
          kernelWeights(R, n, M, j, e)(i)
        intros i hi
        have columnValue := columnWeights.value at R, n, charColumn(R, n, M, j), e, i with *
        have entryValue := charColumn.value at R, n, M, j, i with *
        have kernelValue := kernelWeights.value at R, n, M, j, e, i with *
        cc
      have sameKernel := finiteRingSum.congr with agree
      have vanish := charMatrix.column_sum at R, n, M, j, e with *
      cc
    have contraction := Matrix.contraction_zero at R, n, charAdjugate(R, n, M)[j, k],
      charColumn(R, n, M, j), a with *
    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,
      R.mul, R.one, transposedMatrix(n, n, R.carrier, pairingWeights(R, n, M, k, a)), j with *
    cc
  have sumColumns := finiteRingSum.zero with columns
  have interchange := finiteDoubleSum.interchange at n, n, R.carrier, R.add, R.zero,
    R.neg, R.mul, R.one, pairingWeights(R, n, M, k, a) with *
  unfold finiteDoubleSum at interchange
  cc

end CayleyHamilton