Grace/Cumulus/Algebra/Ring/CayleyHamilton.g17

Open in Workbench Download source

Imports

MatrixPolynomial · Polynomial.Characteristic

Declarations

Source

1-- The Cayley–Hamilton theorem over a bundled commutative ring: the2-- characteristic polynomial charpoly(M) of a square matrix M, an element3-- of polynomialRing(R, {0}), evaluates at M to the zero matrix; the proof4-- reads the adjugate identity of the characteristic matrix inside the5-- commutant of M and contracts it against the columns of M; everything6-- here is ZF7-- Part of Cumulus, the Grace17 mathematics library.8-- Copyright (c) 2026 Grant Passmore.9-- Released under the Apache License 2.0. See LICENSE in the repository root.10-- Authors: Grant Passmore1112module Grace.Cumulus.Algebra.Ring.CayleyHamilton13import MatrixPolynomial14import Polynomial.Characteristic1516notation 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)1718-- The characteristic matrix M · 1 - M̃ of M over its commutant, M̃ the19-- matrix of scalar matrices, and its adjugate there.20def charMatrix (R n M : Set) : Set :=21  characteristicMatrix(n, Ring.carrier(commutant(R, n, M)),22    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),23    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),24    Ring.one(commutant(R, n, M)),25    matrixMap(n, Ring.carrier(R), Ring.carrier(commutant(R, n, M)),26      scalarEmbedding(R, n), M), M)27def charAdjugate (R n M : Set) : Set :=28  adjugate(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),29    Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),30    Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)),31    charMatrix(R, n, M))3233section Polynomials34variable (R : Set) (n : Nat)35hypothesis comm : CommRing(R)3637theorem charpoly.mem (M : R ^ n × n)38  shows charpoly(M) ∈ polynomialRing(R, {0})39proof40  have parts := CommRing.parts with comm41  have square := Matrix.square at M, R, n with assumption42  have shape := squareMatrices.membership.forward with square43  have index : 0 ∈ {0} by simp [singleton.membership]44  have member := characteristicPolynomial.member at {0}, R.carrier, R.add, R.zero,45    R.neg, R.mul, R.one, n, M, 0 with *46  rw polynomialRing.carrierOf47  exact member4849theorem charMatrix.scalars (M : R ^ n × n)50  shows RingMatrix(n, Ring.carrier(commutant(R, n, M)),51    matrixMap(n, Ring.carrier(R), Ring.carrier(commutant(R, n, M)), scalarEmbedding(R, n), M))52proof53  have target := commutant.comm_ring at R, n, M with *54  have hom := scalarEmbedding.hom at R, n, M with *55  have function : scalarEmbedding(R, n) : R.carrier → Ring.carrier(commutant(R, n, M))56    have parts := RingHom.parts with hom57    exact IsRingHom.function with parts58  have square := Matrix.square at M, R, n with assumption59  have shape := squareMatrices.membership.forward with square60  exact matrixMap.matrix with shape, function6162theorem charMatrix.scalar_entry (M : R ^ n × n) (i j : Set)63  requires row : i ∈ n64  requires column : j ∈ n65  shows matrixMap(n, Ring.carrier(R), Ring.carrier(commutant(R, n, M)), scalarEmbedding(R, n), M)[i, j] =66    scalarMatrix(R, n, M[i, j])67proof68  have natural : Nat(n) by typecheck69  have target := commutant.comm_ring at R, n, M with *70  have hom := scalarEmbedding.hom at R, n, M with *71  have function : scalarEmbedding(R, n) : R.carrier → Ring.carrier(commutant(R, n, M))72    have parts := RingHom.parts with hom73    exact IsRingHom.function with parts74  have square := Matrix.square at M, R, n with assumption75  have shape := squareMatrices.membership.forward with square76  have entry := Matrix.entry at M, R, n, i, j with *77  have mapped := matrixMap.entry at n, R.carrier, Ring.carrier(commutant(R, n, M)),78    scalarEmbedding(R, n), M, i, j with *79  have value := scalarEmbedding.value at R, n, M[i, j] with *80  rw mapped81  exact value8283theorem charMatrix.matrix (M : R ^ n × n)84  shows RingMatrix(n, Ring.carrier(commutant(R, n, M)), charMatrix(R, n, M))85proof86  have target := commutant.comm_ring at R, n, M with *87  have targetParts := CommRing.parts with target88  have scalars := charMatrix.scalars at R, n, M with *89  have self := commutant.self_mem at R, n, M with *90  unfold charMatrix91  exact characteristicMatrix.matrix with *9293theorem charMatrix.entry (M : R ^ n × n) (i j : Set)94  requires row : i ∈ n95  requires column : j ∈ n96  shows charMatrix(R, n, M)[i, j] =97    call2(Ring.add(commutant(R, n, M)),98      singleValue(Ring.carrier(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), M, j, i),99      Ring.neg(commutant(R, n, M))(scalarMatrix(R, n, M[i, j])))100proof101  have target := commutant.comm_ring at R, n, M with *102  have targetParts := CommRing.parts with target103  have scalars := charMatrix.scalars at R, n, M with *104  have self := commutant.self_mem at R, n, M with *105  have entry := characteristicMatrix.entry at n, Ring.carrier(commutant(R, n, M)),106    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),107    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),108    Ring.one(commutant(R, n, M)),109    matrixMap(n, Ring.carrier(R), Ring.carrier(commutant(R, n, M)), scalarEmbedding(R, n), M),110    M, i, j with *111  have scalar := charMatrix.scalar_entry at R, n, M, i, j with *112  unfold charMatrix113  cc114115theorem charAdjugate.matrix (M : R ^ n × n)116  shows RingMatrix(n, Ring.carrier(commutant(R, n, M)), charAdjugate(R, n, M))117proof118  have target := commutant.comm_ring at R, n, M with *119  have targetParts := CommRing.parts with target120  have finite := Finite.natural at n121  have matrix := charMatrix.matrix at R, n, M with *122  unfold charAdjugate123  exact adjugate.matrix with *124125end Polynomials126127-- The entries of the terms of a finite sum in the commutant.128defgraph entryWeights (R n M V u a b : Set) (x ∈ V) : Ring.carrier(R) := u(x)[a, b]129requires comm : CommRing(R)130requires natural : Nat(n)131requires matrix : M : R ^ n × n132requires weights : u : V → Ring.carrier(commutant(R, n, M))133requires row : a ∈ n134requires column : b ∈ n135proof136  have value := FunctionBetween.apply_closed with weights, member137  have guard := commutant.mem_matrix with value138  exact Matrix.entry with guard, row, column139140section Sums141variable (R : Set) (n : Nat)142hypothesis comm : CommRing(R)143144theorem indexedRingSum.commutant_entry (M : R ^ n × n) (V u f a b : Set, k : Nat)145  shows (∀ i ∈ k, f(i) ∈ V) → (u : V → Ring.carrier(commutant(R, n, M))) →146    a ∈ n → b ∈ n →147    indexedRingSum(u, f, Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), k)[a, b] =148      indexedRingSum(entryWeights(R, n, M, V, u, a, b), f, R.add, R.zero, k)149proof150  induction k151  | zero =>152    intros positions weights row column153    have zero := commutant.zero_value at R, n, M with *154    have entry := matrixRing.zero_entry at R, n, a, b with *155    rw [indexedRingSum, indexedRingSum, zero]156    exact entry157  | succ(m) using ih =>158    intros positions weights row column159    have natural : Nat(n) by typecheck160    have target := commutant.comm_ring at R, n, M with *161    have targetParts := CommRing.parts with target162    have smaller : ∀ i ∈ m, f(i) ∈ V163      intros i hi164      have next := membership.into_successor at i, m with *165      exact positions with i, next166    have previous := ih with smaller, weights, row, column167    have values : WeightedValues(u, f, Ring.carrier(commutant(R, n, M)), m)168      intros i hi169      have position := smaller with i, hi170      exact FunctionBetween.apply_closed with weights, position171    have closure := indexedRingSum.closed at Ring.carrier(commutant(R, n, M)),172      Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),173      Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),174      Ring.one(commutant(R, n, M)), u, f, m with *175    have prefixIn := closure with values176    have lastPosition := positions with m, membership.self_successor at m with *177    have lastIn := FunctionBetween.apply_closed with weights, lastPosition178    have prefixGuard := commutant.mem_matrix with prefixIn179    have lastGuard := commutant.mem_matrix with lastIn180    have sum := commutant.add_value at R, n, M,181      indexedRingSum(u, f, Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), m),182      u(f(m)) with *183    have entry := matrixRing.add_entry at R, n,184      indexedRingSum(u, f, Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), m),185      u(f(m)), a, b with *186    have graph := entryWeights.function at R, n, M, V, u, a, b with *187    have weight := entryWeights.value at R, n, M, V, u, a, b, f(m) with *188    rw [indexedRingSum, indexedRingSum, sum, entry, previous, weight]189    rfl190191theorem finiteRingSum.commutant_entry (M : R ^ n × n) (V u a b : Set)192  requires finite : Finite(V)193  requires weights : u : V → Ring.carrier(commutant(R, n, M))194  requires row : a ∈ n195  requires column : b ∈ n196  shows finiteRingSum(V, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),197      Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),198      Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), u)[a, b] =199    finiteRingSum(V, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,200      entryWeights(R, n, M, V, u, a, b))201proof202  have natural : Nat(n) by typecheck203  have parts := CommRing.parts with comm204  have target := commutant.comm_ring at R, n, M with *205  have targetParts := CommRing.parts with target206  have graph := entryWeights.function at R, n, M, V, u, a, b with *207  have selected := finiteRingSum.selected at V, Ring.carrier(commutant(R, n, M)),208    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),209    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),210    Ring.one(commutant(R, n, M)), u with *211  obtain ⟨m, naturalM, f, enumeration, equationS⟩ := selected.right212  have injective := Bijective.injective with enumeration213  have function := Injective.function with injective214  have equationR := finiteRingSum.enumeration at V, R.carrier, R.add, R.zero, R.neg,215    R.mul, R.one, entryWeights(R, n, M, V, u, a, b), f, m with *216  have positions : ∀ i ∈ m, f(i) ∈ V217    intros i hi218    exact FunctionBetween.apply_closed with function, hi219  have step := indexedRingSum.commutant_entry at R, n, M, V, u, f, a, b, m with *220  rw [equationS, equationR]221  exact step with positions, weights, row, column222223end Sums224225-- The entries (i, i) of the column j of the characteristic matrix, as226-- matrices, read at row e: the annihilation relation says they sum to 0.227defgraph kernelWeights (R n M j e : Set) (i ∈ n) : Ring.carrier(R) :=228  charMatrix(R, n, M)[i, j][e, i]229requires comm : CommRing(R)230requires natural : Nat(n)231requires matrix : M : R ^ n × n232requires column : j ∈ n233requires row : e ∈ n234proof235  have shape := charMatrix.matrix at R, n, M with *236  have entry := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),237    charMatrix(R, n, M), i, j with *238  have guard := commutant.mem_matrix with entry239  exact Matrix.entry with guard, row, member240241section Kernel242variable (R : Set) (n : Nat)243hypothesis comm : CommRing(R)244245theorem charMatrix.column_sum (M : R ^ n × n) (j e : Set)246  requires column : j ∈ n247  requires row : e ∈ n248  shows finiteRingSum(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,249    kernelWeights(R, n, M, j, e)) = R[0]250proof251  have natural : Nat(n) by typecheck252  have parts := CommRing.parts with comm253  have finite := Finite.natural at n254  have ringT := matrixRing.ring at R, n with *255  have partsT := Ring.parts with ringT256  have target := commutant.comm_ring at R, n, M with *257  have targetParts := CommRing.parts with target258  have targetRing := IsCommRing.ring with targetParts259  have self := commutant.self_mem at R, n, M with *260  have zeroS := commutant.zero_value at R, n, M with *261  have zeroIn : R[0] ∈ R := Ring.zero_mem with *262  have oneIn : R[1] ∈ R := Ring.one_mem with *263  have minusOne : R[-1] ∈ R := Ring.neg_mem with *264  have entryEJ := Matrix.entry at M, R, n, e, j with *265  have weights := kernelWeights.function at R, n, M, j, e with *266  have firstSel := coefficientSingle.function at n, R.carrier, R.zero, M[e, j], j with *267  have secondSel := coefficientSingle.function at n, R.carrier, R.zero, M[e, j], e with *268  have values : ∀ i ∈ n, kernelWeights(R, n, M, j, e)(i) =269      R[1] * coefficientSingle(n, Ring.carrier(R), R.zero, M[e, j], j)(i) +270        R[-1] * coefficientSingle(n, Ring.carrier(R), R.zero, M[e, j], e)(i)271    intros i hi272    have entryIJ := Matrix.entry at M, R, n, i, j with *273    have weight := kernelWeights.value at R, n, M, j, e, i with *274    have entry := charMatrix.entry at R, n, M, i, j with *275    have deltaIn := singleValue.closed at Ring.carrier(commutant(R, n, M)),276      Ring.zero(commutant(R, n, M)), M, j, i with *277    have scalarIn := commutant.scalar_mem at R, n, M, M[i, j] with *278    have negIn := IsRing.neg_closed with targetRing, scalarIn279    have sum := commutant.add_value at R, n, M,280      singleValue(Ring.carrier(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), M, j, i),281      Ring.neg(commutant(R, n, M))(scalarMatrix(R, n, M[i, j])) with *282    have negation := commutant.neg_value at R, n, M, scalarMatrix(R, n, M[i, j]) with *283    have deltaGuard := commutant.mem_matrix with deltaIn284    have scalarGuard := scalarMatrix.guard at R, n, M[i, j] with *285    have scalarMem := Matrix.mem_ring with scalarGuard286    have negMem := IsRing.neg_closed with partsT, scalarMem287    have negGuard := Matrix.of_mem with negMem288    have addEntry := matrixRing.add_entry at R, n,289      singleValue(Ring.carrier(commutant(R, n, M)), Ring.zero(commutant(R, n, M)), M, j, i),290      Ring.neg(matrixRing(R, n))(scalarMatrix(R, n, M[i, j])), e, i with *291    have negEntry := matrixRing.neg_entry at R, n, scalarMatrix(R, n, M[i, j]), e, i with *292    have scalarEntry := scalarMatrix.entry at R, n, M[i, j], e, i with *293    rw [weight, entry, sum, negation, addEntry, negEntry, scalarEntry]294    have alternatives : i = j ∨ i ≠ j by tauto295    cases alternatives with same | different296    . have delta := singleValue.same at Ring.carrier(commutant(R, n, M)),297        Ring.zero(commutant(R, n, M)), M, j, i with *298      have first := coefficientSingle.same at n, R.carrier, R.zero, M[e, j], j with *299      rw [delta, same, first]300      have entryJJ := Matrix.entry at M, R, n, j, j with *301      have alternativesE : e = j ∨ e ≠ j by tauto302      cases alternativesE with sameE | differentE303      . rw sameE304        have reflJ : j = j by rfl305        have unit := singleValue.same at R.carrier, R.zero, R.one, j, j with *306        have second := coefficientSingle.same at n, R.carrier, R.zero, M[j, j], j with *307        rw [unit, second]308        ring309      . have reverse : j ≠ e310          intro equal311          apply differentE312          cc313        have unit := singleValue.other at R.carrier, R.zero, R.one, j, e with *314        have second := coefficientSingle.other at n, R.carrier, R.zero, M[e, j], e, j with *315        rw [unit, second]316        ring317    . have delta := singleValue.other at Ring.carrier(commutant(R, n, M)),318        Ring.zero(commutant(R, n, M)), M, j, i with *319      have zeroEntry := matrixRing.zero_entry at R, n, e, i with *320      have first := coefficientSingle.other at n, R.carrier, R.zero, M[e, j], j, i with *321      rw [delta, zeroS, zeroEntry, first]322      have alternativesE : e = i ∨ e ≠ i by tauto323      cases alternativesE with sameE | differentE324      . rw sameE325        have reflI : i = i by rfl326        have unit := singleValue.same at R.carrier, R.zero, R.one, i, i with *327        have second := coefficientSingle.same at n, R.carrier, R.zero, M[i, j], i with *328        rw [unit, second]329        ring330      . have reverse : i ≠ e331          intro equal332          apply differentE333          cc334        have unit := singleValue.other at R.carrier, R.zero, R.one, i, e with *335        have second := coefficientSingle.other at n, R.carrier, R.zero, M[e, j], e, i with *336        rw [unit, second]337        ring338  have linear := finiteRingSum.linear at n, R.carrier, R.add, R.zero, R.neg, R.mul,339    R.one, coefficientSingle(n, R.carrier, R.zero, M[e, j], j),340    coefficientSingle(n, R.carrier, R.zero, M[e, j], e),341    kernelWeights(R, n, M, j, e), R[1], R[-1] with *342  have first := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg, R.mul,343    R.one, M[e, j], j with *344  have second := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg, R.mul,345    R.one, M[e, j], e with *346  rw [linear, first, second]347  ring348349end Kernel350351-- Contracting a matrix A against a family Q of matrices: the row sums of352-- the products A · Q(i) at the diagonal positions vanish when every353-- column family of Q sums to zero.354defgraph columnWeights (R n Q e : Set) (i ∈ n) : Ring.carrier(R) := Q(i)[e, i]355requires comm : CommRing(R)356requires family : Q : n → Ring.carrier(matrixRing(R, n))357requires row : e ∈ n358proof359  have value := FunctionBetween.apply_closed with family, member360  have guard := Matrix.of_mem with value361  exact Matrix.entry with guard, row, member362363defgraph productWeights (R n A Q a : Set) (i ∈ n) : Ring.carrier(R) :=364  call2(Ring.mul(matrixRing(R, n)), A, Q(i))[a, i]365requires comm : CommRing(R)366requires natural : Nat(n)367requires matrix : A : R ^ n × n368requires family : Q : n → Ring.carrier(matrixRing(R, n))369requires row : a ∈ n370proof371  have ringT := matrixRing.ring at R, n with *372  have value := FunctionBetween.apply_closed with family, member373  have left := Matrix.mem_ring with matrix374  have partsT := Ring.parts with ringT375  have product := IsRing.mul_closed with partsT, left, value376  have guard := Matrix.of_mem with product377  exact Matrix.entry with guard, row, member378379defunique contractionWeightValue (R : Set, n : Nat, A Q a q : Set) (x ∈ Ring.carrier(R)) :=380  ∃ i ∈ n, ∃ e ∈ n, q = (i, e) ∧ x = call2(Ring.mul(R), A[a, e], Q(i)[e, i])381requires comm : CommRing(R)382requires matrix : A : R ^ n × n383requires family : Q : n → Ring.carrier(matrixRing(R, n))384requires row : a ∈ n385requires pair : q ∈ n × n386proof387  obtain ⟨bound, i, hi, e, he, shape⟩ := product.membership.forward at388    n, n, q with *389  have parts := CommRing.parts with comm390  have ordinary := IsCommRing.ring with parts391  have entryA := Matrix.entry at A, R, n, a, e with *392  have value := FunctionBetween.apply_closed with family, hi393  have guard := Matrix.of_mem with value394  have entryQ := Matrix.entry at Q(i), R, n, e, i with *395  have product := IsRing.mul_closed with ordinary, entryA, entryQ396  refine ⟨call2(Ring.mul(R), A[a, e], Q(i)[e, i]), product, i, hi, e, he, shape, rfl⟩397uniqueness398  intros u hu first v hv second399  obtain ⟨i, hi, e, he, shapeU, valueU⟩ := first400  obtain ⟨k, hk, l, hl, shapeV, valueV⟩ := second401  have equal : (i, e) = (k, l)402    cc403  have coordinates := orderedPair.injective at i, e, k, l with equal404  cc405406defgraph contractionWeights (R : Set, n : Nat, A Q a : Set) (q ∈ n × n) : Ring.carrier(R) :=407  contractionWeightValue(R, n, A, Q, a, q)408requires comm : CommRing(R)409requires matrix : A : R ^ n × n410requires family : Q : n → Ring.carrier(matrixRing(R, n))411requires row : a ∈ n412proof413  have selected := contractionWeightValue.selected at R, n, A, Q, a, q with *414  exact selected.left415416theorem contractionWeights.pair (R : Set, n : Nat, A Q a i e : Set)417  requires comm : CommRing(R)418  requires matrix : A : R ^ n × n419  requires family : Q : n → Ring.carrier(matrixRing(R, n))420  requires row : a ∈ n421  requires hi : i ∈ n422  requires he : e ∈ n423  shows contractionWeights(R, n, A, Q, a)((i, e)) = A[a, e] * Q(i)[e, i]424proof425  have pair := product.pair at i, e, n, n with *426  have selected := contractionWeightValue.selected at R, n, A, Q, a, (i, e) with *427  obtain ⟨k, hk, l, hl, shape, result⟩ := selected.right428  have coordinates := orderedPair.injective with shape429  have value := contractionWeights.value at R, n, A, Q, a, (i, e) with *430  cc431432section Contraction433variable (R : Set) (n : Nat)434hypothesis comm : CommRing(R)435436theorem Matrix.contraction_zero (A : R ^ n × n) (Q a : Set)437  requires family : Q : n → Ring.carrier(matrixRing(R, n))438  requires row : a ∈ n439  requires vanishing : ∀ e ∈ n, finiteRingSum(n, R.carrier, R.add, R.zero, R.neg,440    R.mul, R.one, columnWeights(R, n, Q, e)) = R[0]441  shows finiteRingSum(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,442    productWeights(R, n, A, Q, a)) = R[0]443proof444  have natural : Nat(n) by typecheck445  have parts := CommRing.parts with comm446  have finite := Finite.natural at n447  have ringT := matrixRing.ring at R, n with *448  have squareA := Matrix.square at A, R, n with assumption449  have shapeA := squareMatrices.membership.forward with squareA450  have array := contractionWeights.function at R, n, A, Q, a with *451  have transposed := transposedMatrix.function at n, n, R.carrier,452    contractionWeights(R, n, A, Q, a) with *453  have rowsL := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,454    R.mul, R.one, contractionWeights(R, n, A, Q, a) with *455  have rowsR := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,456    R.mul, R.one, transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)) with *457  have products := productWeights.function at R, n, A, Q, a with *458  have leftRows : ∀ i ∈ n, productWeights(R, n, A, Q, a)(i) =459      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, contractionWeights(R, n, A, Q, a))(i)460    intros i hi461    have value := FunctionBetween.apply_closed with family, hi462    have guard := Matrix.of_mem with value463    have squareQ := Matrix.square with guard464    have shapeQ := squareMatrices.membership.forward with squareQ465    have weight := productWeights.value at R, n, A, Q, a, i with *466    have entry := matrixRing.mul_entry at R, n, A, Q(i), a, i with *467    have rowWeights := finiteRowWeights.function at n, n, R.carrier,468      contractionWeights(R, n, A, Q, a), i with *469    have inner := matrixProductWeights.function at n, R.carrier, R.add, R.zero,470      R.neg, R.mul, R.one, A, Q(i), a, i with *471    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) =472        finiteRowWeights(n, n, Ring.carrier(R), contractionWeights(R, n, A, Q, a), i)(e)473      intros e he474      have product := matrixProductWeights.value at n, R.carrier, R.add, R.zero,475        R.neg, R.mul, R.one, A, Q(i), a, i, e with *476      have rowWeight := finiteRowWeights.value at n, n, R.carrier,477        contractionWeights(R, n, A, Q, a), i, e with *478      have cell := contractionWeights.pair at R, n, A, Q, a, i, e with *479      cc480    have same := finiteRingSum.congr with cells481    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,482      R.mul, R.one, contractionWeights(R, n, A, Q, a), i with *483    unfold matrixProductEntry at entry484    cc485  have rightRows : ∀ e ∈ n,486      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]487    intros e he488    have entryA := Matrix.entry at A, R, n, a, e with *489    have rowWeights := finiteRowWeights.function at n, n, R.carrier,490      transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)), e with *491    have columns := columnWeights.function at R, n, Q, e with *492    have scaled : ∀ i ∈ n, finiteRowWeights(n, n, Ring.carrier(R), transposedMatrix(n, n, Ring.carrier(R), contractionWeights(R, n, A, Q, a)), e)(i) =493        A[a, e] * columnWeights(R, n, Q, e)(i)494      intros i hi495      have rowWeight := finiteRowWeights.value at n, n, R.carrier,496        transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)), e, i with *497      have swap := transposedMatrix.pair at n, n, R.carrier,498        contractionWeights(R, n, A, Q, a), i, e with *499      have cell := contractionWeights.pair at R, n, A, Q, a, i, e with *500      have column := columnWeights.value at R, n, Q, e, i with *501      cc502    have scale := finiteRingSum.scale_eq at n, R.carrier, R.add, R.zero, R.neg,503      R.mul, R.one, columnWeights(R, n, Q, e),504      finiteRowWeights(n, n, R.carrier, transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)), e),505      A[a, e] with *506    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,507      R.mul, R.one, transposedMatrix(n, n, R.carrier, contractionWeights(R, n, A, Q, a)), e with *508    have vanish := vanishing with e, he509    rw [rowSum, scale, vanish]510    ring511  have sameL := finiteRingSum.congr with leftRows512  have sumR := finiteRingSum.zero with rightRows513  have interchange := finiteDoubleSum.interchange at n, n, R.carrier, R.add, R.zero,514    R.neg, R.mul, R.one, contractionWeights(R, n, A, Q, a) with *515  unfold finiteDoubleSum at interchange516  cc517518end Contraction519520-- The column j of the characteristic matrix as a family of matrices, the521-- diagonal entries of the adjugate identity read at row a, and the522-- products adj(j, k) · C(i, j) read at (a, i), as an array over n × n.523defgraph charColumn (R n M j : Set) (i ∈ n) : Ring.carrier(matrixRing(R, n)) :=524  charMatrix(R, n, M)[i, j]525requires comm : CommRing(R)526requires natural : Nat(n)527requires matrix : M : R ^ n × n528requires column : j ∈ n529proof530  have shape := charMatrix.matrix at R, n, M with *531  have entry := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),532    charMatrix(R, n, M), i, j with *533  have subset := commutant.subset at R, n, M with *534  exact subset with charMatrix(R, n, M)[i, j], entry535536defgraph diagonalWeights (R n M k a : Set) (i ∈ n) : Ring.carrier(R) :=537  matrixProductEntry(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),538    Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),539    Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)),540    charMatrix(R, n, M), charAdjugate(R, n, M), i, k)[a, i]541requires comm : CommRing(R)542requires natural : Nat(n)543requires matrix : M : R ^ n × n544requires column : k ∈ n545requires row : a ∈ n546proof547  have target := commutant.comm_ring at R, n, M with *548  have targetParts := CommRing.parts with target549  have finite := Finite.natural at n550  have shapeC := charMatrix.matrix at R, n, M with *551  have shapeA := charAdjugate.matrix at R, n, M with *552  have weights := matrixProductWeights.function at n, Ring.carrier(commutant(R, n, M)),553    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),554    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),555    Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k with *556  have closed : matrixProductEntry(n, Ring.carrier(commutant(R, n, M)),557      Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),558      Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),559      Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M),560      i, k) ∈ Ring.carrier(commutant(R, n, M))561    unfold matrixProductEntry562    exact finiteRingSum.closed with *563  have guard := commutant.mem_matrix with closed564  exact Matrix.entry with guard, row, member565566defunique pairingWeightValue (R : Set, n : Nat, M k a q : Set) (x ∈ Ring.carrier(R)) :=567  ∃ i ∈ n, ∃ j ∈ n, q = (i, j) ∧568    x = call2(Ring.mul(matrixRing(R, n)), charAdjugate(R, n, M)[j, k], charMatrix(R, n, M)[i, j])[a, i]569requires comm : CommRing(R)570requires matrix : M : R ^ n × n571requires column : k ∈ n572requires row : a ∈ n573requires pair : q ∈ n × n574proof575  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward at576    n, n, q with *577  have ringT := matrixRing.ring at R, n with *578  have partsT := Ring.parts with ringT579  have shapeC := charMatrix.matrix at R, n, M with *580  have shapeA := charAdjugate.matrix at R, n, M with *581  have subset := commutant.subset at R, n, M with *582  have entryC := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),583    charMatrix(R, n, M), i, j with *584  have entryA := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),585    charAdjugate(R, n, M), j, k with *586  have leftIn := subset with charAdjugate(R, n, M)[j, k], entryA587  have rightIn := subset with charMatrix(R, n, M)[i, j], entryC588  have product := IsRing.mul_closed with partsT, leftIn, rightIn589  have guard := Matrix.of_mem with product590  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 *591  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⟩592uniqueness593  intros u hu first v hv second594  obtain ⟨i, hi, j, hj, shapeU, valueU⟩ := first595  obtain ⟨p, hp, s, hs, shapeV, valueV⟩ := second596  have equal : (i, j) = (p, s)597    cc598  have coordinates := orderedPair.injective at i, j, p, s with equal599  cc600601defgraph pairingWeights (R : Set, n : Nat, M k a : Set) (q ∈ n × n) : Ring.carrier(R) :=602  pairingWeightValue(R, n, M, k, a, q)603requires comm : CommRing(R)604requires matrix : M : R ^ n × n605requires column : k ∈ n606requires row : a ∈ n607proof608  have selected := pairingWeightValue.selected at R, n, M, k, a, q with *609  exact selected.left610611theorem pairingWeights.pair (R : Set, n : Nat, M k a i j : Set)612  requires comm : CommRing(R)613  requires matrix : M : R ^ n × n614  requires column : k ∈ n615  requires row : a ∈ n616  requires hi : i ∈ n617  requires hj : j ∈ n618  shows pairingWeights(R, n, M, k, a)((i, j)) =619    call2(Ring.mul(matrixRing(R, n)), charAdjugate(R, n, M)[j, k], charMatrix(R, n, M)[i, j])[a, i]620proof621  have pair := product.pair at i, j, n, n with *622  have selected := pairingWeightValue.selected at R, n, M, k, a, (i, j) with *623  obtain ⟨p, hp, s, hs, shape, result⟩ := selected.right624  have coordinates := orderedPair.injective with shape625  have value := pairingWeights.value at R, n, M, k, a, (i, j) with *626  cc627628section CayleyHamilton629variable (R : Set) (n : Nat)630hypothesis comm : CommRing(R)631632-- The evaluation of the characteristic polynomial at M is the determinant633-- of the characteristic matrix over the commutant of M.634theorem charpoly.evaluate (M : R ^ n × n)635  shows evalAt(M)(charpoly(M)) = determinant(n, Ring.carrier(commutant(R, n, M)),636    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),637    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),638    Ring.one(commutant(R, n, M)), charMatrix(R, n, M))639proof640  have parts := CommRing.parts with comm641  have target := commutant.comm_ring at R, n, M with *642  have targetParts := CommRing.parts with target643  have hom := scalarEmbedding.hom at R, n, M with *644  have homParts := RingHom.parts with hom645  have self := commutant.self_mem at R, n, M with *646  have assignment := constantFunction.function at {0}, Ring.carrier(commutant(R, n, M)), M with *647  have index : 0 ∈ {0} by simp [singleton.membership]648  have point := constantFunction.apply at {0}, Ring.carrier(commutant(R, n, M)), 0, M with *649  have square := Matrix.square at M, R, n with assumption650  have shape := squareMatrices.membership.forward with square651  have mapped := characteristicPolynomial.evaluate_mapped at {0}, R.carrier, R.add, R.zero,652    R.neg, R.mul, R.one, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),653    Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),654    Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), scalarEmbedding(R, n),655    constantFunction({0}, Ring.carrier(commutant(R, n, M)), M), n, M, 0 with *656  rw point at mapped657  unfold matrixEvaluation658  rw evaluationHom.graph659  unfold charMatrix660  cc661662-- The Cayley–Hamilton theorem: a square matrix satisfies its own663-- characteristic polynomial.664theorem Matrix.cayley_hamilton (M : R ^ n × n)665  shows evalAt(M)(charpoly(M)) = matrixRing(R, n)[0]666proof667  have natural : Nat(n) by typecheck668  have parts := CommRing.parts with comm669  have finite := Finite.natural at n670  have ringT := matrixRing.ring at R, n with *671  have partsT := Ring.parts with ringT672  have target := commutant.comm_ring at R, n, M with *673  have targetParts := CommRing.parts with target674  have subset := commutant.subset at R, n, M with *675  have shapeC := charMatrix.matrix at R, n, M with *676  have shapeA := charAdjugate.matrix at R, n, M with *677  have evaluated := charpoly.evaluate at R, n, M with *678  have determinantIn := determinant.closed at Ring.carrier(commutant(R, n, M)),679    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),680    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),681    Ring.one(commutant(R, n, M)), charMatrix(R, n, M), n with *682  have determinantGuard := commutant.mem_matrix with determinantIn683  have zeroGuard := Matrix.of_mem at matrixRing(R, n)[0], R, n with (Ring.zero_mem with *)684  rw evaluated685  apply Matrix.ext with determinantGuard, zeroGuard686  intros a ha k hk687  have zeroEntry := matrixRing.zero_entry at R, n, a, k with *688  rw zeroEntry689  have determinantEntry := Matrix.entry at determinant(n, Ring.carrier(commutant(R, n, M)),690    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),691    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),692    Ring.one(commutant(R, n, M)), charMatrix(R, n, M)), R, n, a, k with *693  have diagonals := diagonalWeights.function at R, n, M, k, a with *694  have selector := coefficientSingle.function at n, R.carrier, R.zero,695    determinant(n, Ring.carrier(commutant(R, n, M)), Ring.add(commutant(R, n, M)),696      Ring.zero(commutant(R, n, M)), Ring.neg(commutant(R, n, M)),697      Ring.mul(commutant(R, n, M)), Ring.one(commutant(R, n, M)), charMatrix(R, n, M))[a, k], k with *698  have array := pairingWeights.function at R, n, M, k, a with *699  have transposed := transposedMatrix.function at n, n, R.carrier,700    pairingWeights(R, n, M, k, a) with *701  have rowsL := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,702    R.mul, R.one, pairingWeights(R, n, M, k, a) with *703  have rowsR := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,704    R.mul, R.one, transposedMatrix(n, n, R.carrier, pairingWeights(R, n, M, k, a)) with *705  -- The adjugate identity in the commutant, entry by entry at row a.706  have diagonal : ∀ i ∈ n, diagonalWeights(R, n, M, k, a)(i) =707      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)708    intros i hi709    have weight := diagonalWeights.value at R, n, M, k, a, i with *710    have identity := adjugate.right_identity at Ring.carrier(commutant(R, n, M)),711      Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),712      Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),713      Ring.one(commutant(R, n, M)), n, charMatrix(R, n, M), i, k with *714    have unfolded : charAdjugate(R, n, M) = adjugate(n, Ring.carrier(commutant(R, n, M)),715        Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),716        Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),717        Ring.one(commutant(R, n, M)), charMatrix(R, n, M))718      simp [charAdjugate]719    rw [weight, unfolded, identity]720    have zeroIn := IsRing.zero_in_carrier with (IsCommRing.ring with targetParts)721    have alternatives : i = k ∨ i ≠ k by tauto722    cases alternatives with same | different723    . have delta := singleValue.same at Ring.carrier(commutant(R, n, M)),724        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 *725      have selected := coefficientSingle.same at n, R.carrier, R.zero,726        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 *727      rw [delta, same, selected]728      rfl729    . have delta := singleValue.other at Ring.carrier(commutant(R, n, M)),730        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 *731      have selected := coefficientSingle.other at n, R.carrier, R.zero,732        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 *733      have zeroEntryI := matrixRing.zero_entry at R, n, a, i with *734      have zeroS := commutant.zero_value at R, n, M with *735      have zeroEntryS : Ring.zero(commutant(R, n, M))[a, i] = R[0]736        rw zeroS737        exact zeroEntryI738      rw [delta, zeroEntryS, selected]739      rfl740  have sameDiagonal := finiteRingSum.congr with diagonal741  have single := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg, R.mul,742    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 *743  -- The same entries as the row sums of the pairing array.744  have rows : ∀ i ∈ n, diagonalWeights(R, n, M, k, a)(i) =745      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, pairingWeights(R, n, M, k, a))(i)746    intros i hi747    have weight := diagonalWeights.value at R, n, M, k, a, i with *748    have products := matrixProductWeights.function at n, Ring.carrier(commutant(R, n, M)),749      Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),750      Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),751      Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k with *752    have entries := finiteRingSum.commutant_entry at R, n, M, n,753      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),754      a, i with *755    have graph := entryWeights.function at R, n, M, n,756      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),757      a, i with *758    have rowWeights := finiteRowWeights.function at n, n, R.carrier,759      pairingWeights(R, n, M, k, a), i with *760    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) =761        finiteRowWeights(n, n, Ring.carrier(R), pairingWeights(R, n, M, k, a), i)(j)762      intros j hj763      have value := entryWeights.value at R, n, M, n,764        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),765        a, i, j with *766      have product := matrixProductWeights.value at n, Ring.carrier(commutant(R, n, M)),767        Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),768        Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),769        Ring.one(commutant(R, n, M)), charMatrix(R, n, M), charAdjugate(R, n, M), i, k, j with *770      have entryC := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),771        charMatrix(R, n, M), i, j with *772      have entryA := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),773        charAdjugate(R, n, M), j, k with *774      have swap := IsCommRing.mul_comm at Ring.carrier(commutant(R, n, M)),775        Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),776        Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),777        Ring.one(commutant(R, n, M)), charMatrix(R, n, M)[i, j], charAdjugate(R, n, M)[j, k] with *778      have lifted := commutant.mul_value at R, n, M, charAdjugate(R, n, M)[j, k],779        charMatrix(R, n, M)[i, j] with *780      have rowWeight := finiteRowWeights.value at n, n, R.carrier,781        pairingWeights(R, n, M, k, a), i, j with *782      have cell := pairingWeights.pair at R, n, M, k, a, i, j with *783      cc784    have same := finiteRingSum.congr with cells785    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,786      R.mul, R.one, pairingWeights(R, n, M, k, a), i with *787    unfold matrixProductEntry at weight788    cc789  have sameRows := finiteRingSum.congr with rows790  -- Each column sum of the transposed array vanishes by the contraction.791  have columns : ∀ j ∈ n,792      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]793    intros j hj794    have entryA := RingMatrix.entry at n, Ring.carrier(commutant(R, n, M)),795      charAdjugate(R, n, M), j, k with *796    have leftIn := subset with charAdjugate(R, n, M)[j, k], entryA797    have leftGuard := Matrix.of_mem with leftIn798    have family := charColumn.function at R, n, M, j with *799    have productsQ := productWeights.function at R, n, charAdjugate(R, n, M)[j, k],800      charColumn(R, n, M, j), a with *801    have rowWeights := finiteRowWeights.function at n, n, R.carrier,802      transposedMatrix(n, n, R.carrier, pairingWeights(R, n, M, k, a)), j with *803    have cells : ∀ i ∈ n, finiteRowWeights(n, n, Ring.carrier(R), transposedMatrix(n, n, Ring.carrier(R), pairingWeights(R, n, M, k, a)), j)(i) =804        productWeights(R, n, charAdjugate(R, n, M)[j, k], charColumn(R, n, M, j), a)(i)805      intros i hi806      have rowWeight := finiteRowWeights.value at n, n, R.carrier,807        transposedMatrix(n, n, R.carrier, pairingWeights(R, n, M, k, a)), j, i with *808      have swap := transposedMatrix.pair at n, n, R.carrier,809        pairingWeights(R, n, M, k, a), i, j with *810      have cell := pairingWeights.pair at R, n, M, k, a, i, j with *811      have columnValue := charColumn.value at R, n, M, j, i with *812      have productValue := productWeights.value at R, n, charAdjugate(R, n, M)[j, k],813        charColumn(R, n, M, j), a, i with *814      cc815    have same := finiteRingSum.congr with cells816    have vanishing : ∀ e ∈ n, finiteRingSum(n, R.carrier, R.add, R.zero, R.neg, R.mul,817        R.one, columnWeights(R, n, charColumn(R, n, M, j), e)) = R[0]818      intros e he819      have columnsQ := columnWeights.function at R, n, charColumn(R, n, M, j), e with *820      have kernel := kernelWeights.function at R, n, M, j, e with *821      have agree : ∀ i ∈ n, columnWeights(R, n, charColumn(R, n, M, j), e)(i) =822          kernelWeights(R, n, M, j, e)(i)823        intros i hi824        have columnValue := columnWeights.value at R, n, charColumn(R, n, M, j), e, i with *825        have entryValue := charColumn.value at R, n, M, j, i with *826        have kernelValue := kernelWeights.value at R, n, M, j, e, i with *827        cc828      have sameKernel := finiteRingSum.congr with agree829      have vanish := charMatrix.column_sum at R, n, M, j, e with *830      cc831    have contraction := Matrix.contraction_zero at R, n, charAdjugate(R, n, M)[j, k],832      charColumn(R, n, M, j), a with *833    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,834      R.mul, R.one, transposedMatrix(n, n, R.carrier, pairingWeights(R, n, M, k, a)), j with *835    cc836  have sumColumns := finiteRingSum.zero with columns837  have interchange := finiteDoubleSum.interchange at n, n, R.carrier, R.add, R.zero,838    R.neg, R.mul, R.one, pairingWeights(R, n, M, k, a) with *839  unfold finiteDoubleSum at interchange840  cc841842end CayleyHamilton843