Grace/Cumulus/Algebra/Ring/MatrixRing.g17

Open in Workbench Download source

Imports

DeterminantIdentity · Basic

Declarations

Source

1-- Bundled matrix rings: the ring value matrixRing(R, n) of the n × n2-- matrices over a bundled commutative ring R, its ring instance, the3-- entries of sums and products, and the determinant and adjugate of a4-- square matrix read off the ring; everything here is ZF5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Ring.MatrixRing11import DeterminantIdentity12import Basic1314-- The n × n matrices over R are the functions on the square of indices.15def squareMatrices (R n : Set) : Set := functionSpace(n × n, Ring.carrier(R))1617theorem squareMatrices.membership (R n M : Set)18  shows M ∈ squareMatrices(R, n) ↔ RingMatrix(n, Ring.carrier(R), M)19proof20  simp [squareMatrices, RingMatrix, functionSpace.mem_iff]2122theorem squareMatrices.function (R n M : Set)23  requires matrix : M ∈ squareMatrices(R, n)24  shows M : n × n → Ring.carrier(R)25proof26  have shape := squareMatrices.membership.forward with matrix27  unfold RingMatrix at shape28  exact shape2930theorem squareMatrices.of_function (R n M : Set)31  requires function : M : n × n → Ring.carrier(R)32  shows M ∈ squareMatrices(R, n)33proof34  have shape : RingMatrix(n, Ring.carrier(R), M) by exact function35  exact squareMatrices.membership.backward with shape3637-- The entrywise sum of two matrices.38defgraph matrixSum (R n M N : Set) (p ∈ n × n) : Ring.carrier(R) := M(p) + N(p)39requires ring : Ring(R)40requires matrixM : M ∈ squareMatrices(R, n)41requires matrixN : N ∈ squareMatrices(R, n)42proof43  have functionM := squareMatrices.function with matrixM44  have functionN := squareMatrices.function with matrixN45  have left := FunctionBetween.apply_closed with functionM, member46  have right := FunctionBetween.apply_closed with functionN, member47  exact Ring.add_mem with *4849theorem matrixSum.entry (R n M N i j : Set)50  requires ring : Ring(R)51  requires matrixM : M ∈ squareMatrices(R, n)52  requires matrixN : N ∈ squareMatrices(R, n)53  requires row : i ∈ n54  requires column : j ∈ n55  shows matrixSum(R, n, M, N)[i, j] = M[i, j] + N[i, j]56proof57  have pair := product.pair at i, j, n, n with *58  exact matrixSum.value at R, n, M, N, (i, j) with *5960theorem matrixSum.matrix (R n M N : Set)61  requires ring : Ring(R)62  requires matrixM : M ∈ squareMatrices(R, n)63  requires matrixN : N ∈ squareMatrices(R, n)64  shows matrixSum(R, n, M, N) ∈ squareMatrices(R, n)65proof66  have function := matrixSum.function at R, n, M, N with *67  exact squareMatrices.of_function with function6869-- The entrywise negation of a matrix.70defgraph matrixNegative (R n M : Set) (p ∈ n × n) : Ring.carrier(R) := -M(p)71requires ring : Ring(R)72requires matrix : M ∈ squareMatrices(R, n)73proof74  have function := squareMatrices.function with matrix75  have entry := FunctionBetween.apply_closed with function, member76  exact Ring.neg_mem with *7778theorem matrixNegative.entry (R n M i j : Set)79  requires ring : Ring(R)80  requires matrix : M ∈ squareMatrices(R, n)81  requires row : i ∈ n82  requires column : j ∈ n83  shows matrixNegative(R, n, M)[i, j] = -M[i, j]84proof85  have pair := product.pair at i, j, n, n with *86  exact matrixNegative.value at R, n, M, (i, j) with *8788theorem matrixNegative.matrix (R n M : Set)89  requires ring : Ring(R)90  requires matrix : M ∈ squareMatrices(R, n)91  shows matrixNegative(R, n, M) ∈ squareMatrices(R, n)92proof93  have function := matrixNegative.function at R, n, M with *94  exact squareMatrices.of_function with function9596-- The product, entry by entry the finite sum of the engine.97defunique matrixProductValue (R : Set, n : Nat, M N p : Set) (a ∈ Ring.carrier(R)) :=98  ∃ i ∈ n, ∃ j ∈ n, p = (i, j) ∧99    a = matrixProductEntry(n, Ring.carrier(R), Ring.add(R), Ring.zero(R),100      Ring.neg(R), Ring.mul(R), Ring.one(R), M, N, i, j)101requires comm : CommRing(R)102requires matrixM : M ∈ squareMatrices(R, n)103requires matrixN : N ∈ squareMatrices(R, n)104requires pair : p ∈ n × n105proof106  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward at107    n, n, p with *108  have parts := CommRing.parts with comm109  have shapeM := squareMatrices.membership.forward with matrixM110  have shapeN := squareMatrices.membership.forward with matrixN111  have weights := matrixProductWeights.function at n, R.carrier, R.add, R.zero,112    R.neg, R.mul, R.one, M, N, i, j with *113  have finiteN := Finite.natural at n114  have finite := Finite.product with finiteN, finiteN115  have value : matrixProductEntry(n, R.carrier, R.add, R.zero, R.neg, R.mul,116      R.one, M, N, i, j) ∈ R.carrier117    unfold matrixProductEntry118    exact finiteRingSum.closed with *119  refine ⟨matrixProductEntry(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,120    M, N, i, j), value, i, hi, j, hj, shape, rfl⟩121uniqueness122  intros u hu first v hv second123  obtain ⟨i, hi, j, hj, shapeU, valueU⟩ := first124  obtain ⟨k, hk, l, hl, shapeV, valueV⟩ := second125  have equal : (i, j) = (k, l)126    cc127  have coordinates := orderedPair.injective at i, j, k, l with equal128  cc129130defgraph matrixProduct (R : Set, n : Nat, M N : Set) (p ∈ n × n) : Ring.carrier(R) :=131  matrixProductValue(R, n, M, N, p)132requires comm : CommRing(R)133requires matrixM : M ∈ squareMatrices(R, n)134requires matrixN : N ∈ squareMatrices(R, n)135proof136  have selected := matrixProductValue.selected at R, n, M, N, p with *137  exact selected.left138139theorem matrixProduct.entry (R : Set, n : Nat, M N i j : Set)140  requires comm : CommRing(R)141  requires matrixM : M ∈ squareMatrices(R, n)142  requires matrixN : N ∈ squareMatrices(R, n)143  requires row : i ∈ n144  requires column : j ∈ n145  shows matrixProduct(R, n, M, N)[i, j] =146    matrixProductEntry(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,147      M, N, i, j)148proof149  have pair := product.pair at i, j, n, n with *150  have selected := matrixProductValue.selected at R, n, M, N, (i, j) with *151  obtain ⟨k, hk, l, hl, shape, result⟩ := selected.right152  have coordinates := orderedPair.injective with shape153  have value := matrixProduct.value at R, n, M, N, (i, j) with *154  cc155156theorem matrixProduct.matrix (R : Set, n : Nat, M N : Set)157  requires comm : CommRing(R)158  requires matrixM : M ∈ squareMatrices(R, n)159  requires matrixN : N ∈ squareMatrices(R, n)160  shows matrixProduct(R, n, M, N) ∈ squareMatrices(R, n)161proof162  have function := matrixProduct.function at R, n, M, N with *163  exact squareMatrices.of_function with function164165-- The operations as graphs on the matrices, the data of the ring value.166defunique matrixAdditionValue (R n q : Set) (S ∈ squareMatrices(R, n)) :=167  ∃ M ∈ squareMatrices(R, n), ∃ N ∈ squareMatrices(R, n),168    q = (M, N) ∧ S = matrixSum(R, n, M, N)169requires ring : Ring(R)170requires pair : q ∈ squareMatrices(R, n) × squareMatrices(R, n)171proof172  obtain ⟨bound, M, hM, N, hN, shape⟩ := product.membership.forward at173    squareMatrices(R, n), squareMatrices(R, n), q with *174  have value := matrixSum.matrix at R, n, M, N with *175  refine ⟨matrixSum(R, n, M, N), value, M, hM, N, hN, shape, rfl⟩176uniqueness177  intros u hu first v hv second178  obtain ⟨M, hM, N, hN, shapeU, valueU⟩ := first179  obtain ⟨K, hK, L, hL, shapeV, valueV⟩ := second180  have equal : (M, N) = (K, L)181    cc182  have coordinates := orderedPair.injective at M, N, K, L with equal183  cc184185defgraph matrixAddition (R n : Set) (q ∈ squareMatrices(R, n) × squareMatrices(R, n)) :186    squareMatrices(R, n) :=187  matrixAdditionValue(R, n, q)188requires ring : Ring(R)189proof190  have selected := matrixAdditionValue.selected at R, n, q with *191  exact selected.left192193theorem matrixAddition.apply (R n M N : Set)194  requires ring : Ring(R)195  requires matrixM : M ∈ squareMatrices(R, n)196  requires matrixN : N ∈ squareMatrices(R, n)197  shows matrixAddition(R, n)(M, N) = matrixSum(R, n, M, N)198proof199  have pair := product.pair at M, N, squareMatrices(R, n), squareMatrices(R, n) with *200  have selected := matrixAdditionValue.selected at R, n, (M, N) with *201  obtain ⟨K, hK, L, hL, shape, result⟩ := selected.right202  have coordinates := orderedPair.injective with shape203  have value := matrixAddition.value at R, n, (M, N) with *204  unfold call2205  cc206207defunique matrixMultiplicationValue (R : Set, n : Nat, q : Set) (S ∈ squareMatrices(R, n)) :=208  ∃ M ∈ squareMatrices(R, n), ∃ N ∈ squareMatrices(R, n),209    q = (M, N) ∧ S = matrixProduct(R, n, M, N)210requires comm : CommRing(R)211requires pair : q ∈ squareMatrices(R, n) × squareMatrices(R, n)212proof213  obtain ⟨bound, M, hM, N, hN, shape⟩ := product.membership.forward at214    squareMatrices(R, n), squareMatrices(R, n), q with *215  have value := matrixProduct.matrix at R, n, M, N with *216  refine ⟨matrixProduct(R, n, M, N), value, M, hM, N, hN, shape, rfl⟩217uniqueness218  intros u hu first v hv second219  obtain ⟨M, hM, N, hN, shapeU, valueU⟩ := first220  obtain ⟨K, hK, L, hL, shapeV, valueV⟩ := second221  have equal : (M, N) = (K, L)222    cc223  have coordinates := orderedPair.injective at M, N, K, L with equal224  cc225226defgraph matrixMultiplication (R : Set, n : Nat) (q ∈ squareMatrices(R, n) × squareMatrices(R, n)) :227    squareMatrices(R, n) :=228  matrixMultiplicationValue(R, n, q)229requires comm : CommRing(R)230proof231  have selected := matrixMultiplicationValue.selected at R, n, q with *232  exact selected.left233234theorem matrixMultiplication.apply (R : Set, n : Nat, M N : Set)235  requires comm : CommRing(R)236  requires matrixM : M ∈ squareMatrices(R, n)237  requires matrixN : N ∈ squareMatrices(R, n)238  shows matrixMultiplication(R, n)(M, N) = matrixProduct(R, n, M, N)239proof240  have pair := product.pair at M, N, squareMatrices(R, n), squareMatrices(R, n) with *241  have selected := matrixMultiplicationValue.selected at R, n, (M, N) with *242  obtain ⟨K, hK, L, hL, shape, result⟩ := selected.right243  have coordinates := orderedPair.injective with shape244  have value := matrixMultiplication.value at R, n, (M, N) with *245  unfold call2246  cc247248defgraph matrixNegation (R n : Set) (M ∈ squareMatrices(R, n)) : squareMatrices(R, n) :=249  matrixNegative(R, n, M)250requires ring : Ring(R)251proof252  exact matrixNegative.matrix at R, n, M with *253254-- The zero matrix and the identity matrix of the engine.255def zeroMatrix (R n : Set) : Set :=256  constantFunction(n × n, Ring.carrier(R), Ring.zero(R))257def oneMatrix (R n : Set) : Set :=258  identityMatrix(n, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R),259    Ring.mul(R), Ring.one(R))260261-- The matrix ring itself.262def matrixRing (R n : Set) : Set :=263  Ring.mk(squareMatrices(R, n), matrixAddition(R, n), zeroMatrix(R, n),264    matrixNegation(R, n), matrixMultiplication(R, n), oneMatrix(R, n))265266theorem matrixRing.carrierOf (R n : Set)267  shows Ring.carrier(matrixRing(R, n)) = squareMatrices(R, n)268proof269  simp [matrixRing, Ring.mk.carrier]270271theorem matrixRing.addOf (R n : Set)272  shows Ring.add(matrixRing(R, n)) = matrixAddition(R, n)273proof274  simp [matrixRing, Ring.mk.add]275276theorem matrixRing.zeroOf (R n : Set)277  shows Ring.zero(matrixRing(R, n)) = zeroMatrix(R, n)278proof279  simp [matrixRing, Ring.mk.zero]280281theorem matrixRing.negOf (R n : Set)282  shows Ring.neg(matrixRing(R, n)) = matrixNegation(R, n)283proof284  simp [matrixRing, Ring.mk.neg]285286theorem matrixRing.mulOf (R n : Set)287  shows Ring.mul(matrixRing(R, n)) = matrixMultiplication(R, n)288proof289  simp [matrixRing, Ring.mk.mul]290291theorem matrixRing.oneOf (R n : Set)292  shows Ring.one(matrixRing(R, n)) = oneMatrix(R, n)293proof294  simp [matrixRing, Ring.mk.one]295296section Constants297variable (R : Set) (n : Nat)298hypothesis comm : CommRing(R)299notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)300301theorem zeroMatrix.matrix302  shows zeroMatrix(R, n) ∈ squareMatrices(R, n)303proof304  have zeroIn : R[0] ∈ R := Ring.zero_mem with *305  have function := constantFunction.function at n × n, R.carrier, R.zero with *306  unfold zeroMatrix307  exact squareMatrices.of_function with function308309theorem zeroMatrix.entry (i j : Set)310  requires row : i ∈ n311  requires column : j ∈ n312  shows zeroMatrix(R, n)[i, j] = R[0]313proof314  have zeroIn : R[0] ∈ R := Ring.zero_mem with *315  have pair := product.pair at i, j, n, n with *316  unfold zeroMatrix317  exact constantFunction.apply with *318319theorem oneMatrix.matrix320  shows oneMatrix(R, n) ∈ squareMatrices(R, n)321proof322  have parts := CommRing.parts with comm323  have shape := identityMatrix.matrix at R.carrier, R.add, R.zero, R.neg,324    R.mul, R.one, n with *325  unfold oneMatrix326  exact squareMatrices.membership.backward with shape327328theorem oneMatrix.entry (i j : Set)329  requires row : i ∈ n330  requires column : j ∈ n331  shows oneMatrix(R, n)[i, j] = singleValue(R.carrier, R.zero, R.one, j, i)332proof333  have parts := CommRing.parts with comm334  unfold oneMatrix335  exact identityMatrix.entry with *336337theorem squareMatrices.entry (M i j : Set)338  requires matrix : M ∈ squareMatrices(R, n)339  requires row : i ∈ n340  requires column : j ∈ n341  shows M[i, j] ∈ R342proof343  have function := squareMatrices.function with matrix344  have pair := product.pair at i, j, n, n with *345  exact FunctionBetween.apply_closed with function, pair346347theorem squareMatrices.ext (M N : Set)348  requires matrixM : M ∈ squareMatrices(R, n)349  requires matrixN : N ∈ squareMatrices(R, n)350  requires entries : ∀ i ∈ n, ∀ j ∈ n, M[i, j] = N[i, j]351  shows M = N352proof353  have shapeM := squareMatrices.membership.forward with matrixM354  have shapeN := squareMatrices.membership.forward with matrixN355  exact RingMatrix.ext with shapeM, shapeN, entries356357end Constants358359section AdditiveLaws360variable (R : Set) (n : Nat)361hypothesis comm : CommRing(R)362363theorem matrixSum.comm (M N : Set)364  requires matrixM : M ∈ squareMatrices(R, n)365  requires matrixN : N ∈ squareMatrices(R, n)366  shows matrixSum(R, n, M, N) = matrixSum(R, n, N, M)367proof368  have left := matrixSum.matrix at R, n, M, N with *369  have right := matrixSum.matrix at R, n, N, M with *370  apply squareMatrices.ext with left, right371  intros i hi j hj372  have entryM := squareMatrices.entry at R, n, M, i, j with *373  have entryN := squareMatrices.entry at R, n, N, i, j with *374  have first := matrixSum.entry at R, n, M, N, i, j with *375  have second := matrixSum.entry at R, n, N, M, i, j with *376  rw [first, second]377  ring378379theorem matrixSum.assoc (M N P : Set)380  requires matrixM : M ∈ squareMatrices(R, n)381  requires matrixN : N ∈ squareMatrices(R, n)382  requires matrixP : P ∈ squareMatrices(R, n)383  shows matrixSum(R, n, matrixSum(R, n, M, N), P) =384    matrixSum(R, n, M, matrixSum(R, n, N, P))385proof386  have sumMN := matrixSum.matrix at R, n, M, N with *387  have sumNP := matrixSum.matrix at R, n, N, P with *388  have left := matrixSum.matrix at R, n, matrixSum(R, n, M, N), P with *389  have right := matrixSum.matrix at R, n, M, matrixSum(R, n, N, P) with *390  apply squareMatrices.ext with left, right391  intros i hi j hj392  have entryM := squareMatrices.entry at R, n, M, i, j with *393  have entryN := squareMatrices.entry at R, n, N, i, j with *394  have entryP := squareMatrices.entry at R, n, P, i, j with *395  have innerL := matrixSum.entry at R, n, M, N, i, j with *396  have innerR := matrixSum.entry at R, n, N, P, i, j with *397  have outerL := matrixSum.entry at R, n, matrixSum(R, n, M, N), P, i, j with *398  have outerR := matrixSum.entry at R, n, M, matrixSum(R, n, N, P), i, j with *399  rw [outerL, outerR, innerL, innerR]400  ring401402theorem matrixSum.zero_left (M : Set)403  requires matrix : M ∈ squareMatrices(R, n)404  shows matrixSum(R, n, zeroMatrix(R, n), M) = M405proof406  have zero := zeroMatrix.matrix at R, n with *407  have sum := matrixSum.matrix at R, n, zeroMatrix(R, n), M with *408  apply squareMatrices.ext with sum, matrix409  intros i hi j hj410  have entryM := squareMatrices.entry at R, n, M, i, j with *411  have entryZ := zeroMatrix.entry at R, n, i, j with *412  have entry := matrixSum.entry at R, n, zeroMatrix(R, n), M, i, j with *413  rw [entry, entryZ]414  ring415416theorem matrixSum.zero_right (M : Set)417  requires matrix : M ∈ squareMatrices(R, n)418  shows matrixSum(R, n, M, zeroMatrix(R, n)) = M419proof420  have zero := zeroMatrix.matrix at R, n with *421  have sum := matrixSum.matrix at R, n, M, zeroMatrix(R, n) with *422  apply squareMatrices.ext with sum, matrix423  intros i hi j hj424  have entryM := squareMatrices.entry at R, n, M, i, j with *425  have entryZ := zeroMatrix.entry at R, n, i, j with *426  have entry := matrixSum.entry at R, n, M, zeroMatrix(R, n), i, j with *427  rw [entry, entryZ]428  ring429430theorem matrixSum.neg_left (M : Set)431  requires matrix : M ∈ squareMatrices(R, n)432  shows matrixSum(R, n, matrixNegative(R, n, M), M) = zeroMatrix(R, n)433proof434  have zero := zeroMatrix.matrix at R, n with *435  have negative := matrixNegative.matrix at R, n, M with *436  have sum := matrixSum.matrix at R, n, matrixNegative(R, n, M), M with *437  apply squareMatrices.ext with sum, zero438  intros i hi j hj439  have entryM := squareMatrices.entry at R, n, M, i, j with *440  have entryZ := zeroMatrix.entry at R, n, i, j with *441  have entryN := matrixNegative.entry at R, n, M, i, j with *442  have entry := matrixSum.entry at R, n, matrixNegative(R, n, M), M, i, j with *443  rw [entry, entryN, entryZ]444  ring445446theorem matrixSum.neg_right (M : Set)447  requires matrix : M ∈ squareMatrices(R, n)448  shows matrixSum(R, n, M, matrixNegative(R, n, M)) = zeroMatrix(R, n)449proof450  have zero := zeroMatrix.matrix at R, n with *451  have negative := matrixNegative.matrix at R, n, M with *452  have sum := matrixSum.matrix at R, n, M, matrixNegative(R, n, M) with *453  apply squareMatrices.ext with sum, zero454  intros i hi j hj455  have entryM := squareMatrices.entry at R, n, M, i, j with *456  have entryZ := zeroMatrix.entry at R, n, i, j with *457  have entryN := matrixNegative.entry at R, n, M, i, j with *458  have entry := matrixSum.entry at R, n, M, matrixNegative(R, n, M), i, j with *459  rw [entry, entryN, entryZ]460  ring461462end AdditiveLaws463464section MultiplicativeLaws465variable (R : Set) (n : Nat)466hypothesis comm : CommRing(R)467notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)468469theorem matrixProduct.entry_sum (M N i j : Set)470  requires matrixM : M ∈ squareMatrices(R, n)471  requires matrixN : N ∈ squareMatrices(R, n)472  requires row : i ∈ n473  requires column : j ∈ n474  shows matrixProduct(R, n, M, N)[i, j] =475    finiteRingSum(n, K, matrixProductWeights(n, K, M, N, i, j))476proof477  have entry := matrixProduct.entry at R, n, M, N, i, j with *478  rw entry479  unfold matrixProductEntry480  rfl481482theorem matrixProduct.one_right (M : Set)483  requires matrix : M ∈ squareMatrices(R, n)484  shows matrixProduct(R, n, M, oneMatrix(R, n)) = M485proof486  have parts := CommRing.parts with comm487  have one := oneMatrix.matrix at R, n with *488  have product := matrixProduct.matrix at R, n, M, oneMatrix(R, n) with *489  have shapeM := squareMatrices.membership.forward with matrix490  have shapeOne := squareMatrices.membership.forward with one491  have finite := Finite.natural at n492  apply squareMatrices.ext with product, matrix493  intros i hi j hj494  have entryM := squareMatrices.entry at R, n, M, i, j with *495  have weights := matrixProductWeights.function at n, R.carrier, R.add, R.zero,496    R.neg, R.mul, R.one, M, oneMatrix(R, n), i, j with *497  have selector := coefficientSingle.function at n, R.carrier, R.zero, M[i, j], j with *498  have values : ∀ k ∈ n, matrixProductWeights(n, K, M, oneMatrix(R, n), i, j)(k) =499      coefficientSingle(n, R.carrier, R.zero, M[i, j], j)(k)500    intros k hk501    have entryK := squareMatrices.entry at R, n, M, i, k with *502    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,503      R.neg, R.mul, R.one, M, oneMatrix(R, n), i, j, k with *504    have unit := oneMatrix.entry at R, n, k, j with *505    have alternatives : k = j ∨ k ≠ j by tauto506    cases alternatives with same | different507    . have delta := singleValue.same at R.carrier, R.zero, R.one, j, k with *508      have selected := coefficientSingle.same at n, R.carrier, R.zero, M[i, j], j with *509      rw [weight, unit, delta, same, selected]510      ring511    . have delta := singleValue.other at R.carrier, R.zero, R.one, j, k with *512      have selected := coefficientSingle.other at n, R.carrier, R.zero, M[i, j], j, k with *513      rw [weight, unit, delta, selected]514      ring515  have same := finiteRingSum.congr with values516  have single := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg,517    R.mul, R.one, M[i, j], j with *518  have entry := matrixProduct.entry_sum at R, n, M, oneMatrix(R, n), i, j with *519  cc520521theorem matrixProduct.one_left (M : Set)522  requires matrix : M ∈ squareMatrices(R, n)523  shows matrixProduct(R, n, oneMatrix(R, n), M) = M524proof525  have parts := CommRing.parts with comm526  have one := oneMatrix.matrix at R, n with *527  have product := matrixProduct.matrix at R, n, oneMatrix(R, n), M with *528  have shapeM := squareMatrices.membership.forward with matrix529  have shapeOne := squareMatrices.membership.forward with one530  have finite := Finite.natural at n531  apply squareMatrices.ext with product, matrix532  intros i hi j hj533  have entryM := squareMatrices.entry at R, n, M, i, j with *534  have weights := matrixProductWeights.function at n, R.carrier, R.add, R.zero,535    R.neg, R.mul, R.one, oneMatrix(R, n), M, i, j with *536  have selector := coefficientSingle.function at n, R.carrier, R.zero, M[i, j], i with *537  have values : ∀ k ∈ n, matrixProductWeights(n, K, oneMatrix(R, n), M, i, j)(k) =538      coefficientSingle(n, R.carrier, R.zero, M[i, j], i)(k)539    intros k hk540    have entryK := squareMatrices.entry at R, n, M, k, j with *541    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,542      R.neg, R.mul, R.one, oneMatrix(R, n), M, i, j, k with *543    have unit := oneMatrix.entry at R, n, i, k with *544    have alternatives : k = i ∨ k ≠ i by tauto545    cases alternatives with same | different546    . have equal : i = k by cc547      have delta := singleValue.same at R.carrier, R.zero, R.one, k, i with *548      have selected := coefficientSingle.same at n, R.carrier, R.zero, M[i, j], i with *549      rw [weight, unit, delta, same, selected]550      ring551    . have reverse : i ≠ k552        intro equal553        apply different554        cc555      have delta := singleValue.other at R.carrier, R.zero, R.one, k, i with *556      have selected := coefficientSingle.other at n, R.carrier, R.zero, M[i, j], i, k with *557      rw [weight, unit, delta, selected]558      ring559  have same := finiteRingSum.congr with values560  have single := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg,561    R.mul, R.one, M[i, j], i with *562  have entry := matrixProduct.entry_sum at R, n, oneMatrix(R, n), M, i, j with *563  cc564565theorem matrixProduct.sum_left (M N P : Set)566  requires matrixM : M ∈ squareMatrices(R, n)567  requires matrixN : N ∈ squareMatrices(R, n)568  requires matrixP : P ∈ squareMatrices(R, n)569  shows matrixProduct(R, n, matrixSum(R, n, M, N), P) =570    matrixSum(R, n, matrixProduct(R, n, M, P), matrixProduct(R, n, N, P))571proof572  have parts := CommRing.parts with comm573  have sum := matrixSum.matrix at R, n, M, N with *574  have productM := matrixProduct.matrix at R, n, M, P with *575  have productN := matrixProduct.matrix at R, n, N, P with *576  have left := matrixProduct.matrix at R, n, matrixSum(R, n, M, N), P with *577  have right := matrixSum.matrix at R, n, matrixProduct(R, n, M, P),578    matrixProduct(R, n, N, P) with *579  have shapeM := squareMatrices.membership.forward with matrixM580  have shapeN := squareMatrices.membership.forward with matrixN581  have shapeP := squareMatrices.membership.forward with matrixP582  have shapeSum := squareMatrices.membership.forward with sum583  have finite := Finite.natural at n584  have oneIn : R[1] ∈ R := Ring.one_mem with *585  apply squareMatrices.ext with left, right586  intros i hi j hj587  have weightsM := matrixProductWeights.function at n, R.carrier, R.add, R.zero,588    R.neg, R.mul, R.one, M, P, i, j with *589  have weightsN := matrixProductWeights.function at n, R.carrier, R.add, R.zero,590    R.neg, R.mul, R.one, N, P, i, j with *591  have weightsSum := matrixProductWeights.function at n, R.carrier, R.add, R.zero,592    R.neg, R.mul, R.one, matrixSum(R, n, M, N), P, i, j with *593  have values : ∀ k ∈ n, matrixProductWeights(n, K, matrixSum(R, n, M, N), P, i, j)(k) =594      R[1] * matrixProductWeights(n, K, M, P, i, j)(k) + R[1] * matrixProductWeights(n, K, N, P, i, j)(k)595    intros k hk596    have entryM := squareMatrices.entry at R, n, M, i, k with *597    have entryN := squareMatrices.entry at R, n, N, i, k with *598    have entryP := squareMatrices.entry at R, n, P, k, j with *599    have weightM := matrixProductWeights.value at n, R.carrier, R.add, R.zero,600      R.neg, R.mul, R.one, M, P, i, j, k with *601    have weightN := matrixProductWeights.value at n, R.carrier, R.add, R.zero,602      R.neg, R.mul, R.one, N, P, i, j, k with *603    have weightSum := matrixProductWeights.value at n, R.carrier, R.add, R.zero,604      R.neg, R.mul, R.one, matrixSum(R, n, M, N), P, i, j, k with *605    have entrySum := matrixSum.entry at R, n, M, N, i, k with *606    rw [weightM, weightN, weightSum, entrySum]607    ring608  have linear := finiteRingSum.linear at n, R.carrier, R.add, R.zero, R.neg,609    R.mul, R.one, matrixProductWeights(n, K, M, P, i, j),610    matrixProductWeights(n, K, N, P, i, j),611    matrixProductWeights(n, K, matrixSum(R, n, M, N), P, i, j), R[1], R[1] with *612  have closedM := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,613    R.mul, R.one, matrixProductWeights(n, K, M, P, i, j) with *614  have closedN := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,615    R.mul, R.one, matrixProductWeights(n, K, N, P, i, j) with *616  have entryL := matrixProduct.entry_sum at R, n, matrixSum(R, n, M, N), P, i, j with *617  have entryM := matrixProduct.entry_sum at R, n, M, P, i, j with *618  have entryN := matrixProduct.entry_sum at R, n, N, P, i, j with *619  have entryR := matrixSum.entry at R, n, matrixProduct(R, n, M, P),620    matrixProduct(R, n, N, P), i, j with *621  rw [entryL, entryR, entryM, entryN, linear]622  ring623624theorem matrixProduct.sum_right (M N P : Set)625  requires matrixM : M ∈ squareMatrices(R, n)626  requires matrixN : N ∈ squareMatrices(R, n)627  requires matrixP : P ∈ squareMatrices(R, n)628  shows matrixProduct(R, n, M, matrixSum(R, n, N, P)) =629    matrixSum(R, n, matrixProduct(R, n, M, N), matrixProduct(R, n, M, P))630proof631  have parts := CommRing.parts with comm632  have sum := matrixSum.matrix at R, n, N, P with *633  have productN := matrixProduct.matrix at R, n, M, N with *634  have productP := matrixProduct.matrix at R, n, M, P with *635  have left := matrixProduct.matrix at R, n, M, matrixSum(R, n, N, P) with *636  have right := matrixSum.matrix at R, n, matrixProduct(R, n, M, N),637    matrixProduct(R, n, M, P) with *638  have shapeM := squareMatrices.membership.forward with matrixM639  have shapeN := squareMatrices.membership.forward with matrixN640  have shapeP := squareMatrices.membership.forward with matrixP641  have shapeSum := squareMatrices.membership.forward with sum642  have finite := Finite.natural at n643  have oneIn : R[1] ∈ R := Ring.one_mem with *644  apply squareMatrices.ext with left, right645  intros i hi j hj646  have weightsN := matrixProductWeights.function at n, R.carrier, R.add, R.zero,647    R.neg, R.mul, R.one, M, N, i, j with *648  have weightsP := matrixProductWeights.function at n, R.carrier, R.add, R.zero,649    R.neg, R.mul, R.one, M, P, i, j with *650  have weightsSum := matrixProductWeights.function at n, R.carrier, R.add, R.zero,651    R.neg, R.mul, R.one, M, matrixSum(R, n, N, P), i, j with *652  have values : ∀ k ∈ n, matrixProductWeights(n, K, M, matrixSum(R, n, N, P), i, j)(k) =653      R[1] * matrixProductWeights(n, K, M, N, i, j)(k) + R[1] * matrixProductWeights(n, K, M, P, i, j)(k)654    intros k hk655    have entryM := squareMatrices.entry at R, n, M, i, k with *656    have entryN := squareMatrices.entry at R, n, N, k, j with *657    have entryP := squareMatrices.entry at R, n, P, k, j with *658    have weightN := matrixProductWeights.value at n, R.carrier, R.add, R.zero,659      R.neg, R.mul, R.one, M, N, i, j, k with *660    have weightP := matrixProductWeights.value at n, R.carrier, R.add, R.zero,661      R.neg, R.mul, R.one, M, P, i, j, k with *662    have weightSum := matrixProductWeights.value at n, R.carrier, R.add, R.zero,663      R.neg, R.mul, R.one, M, matrixSum(R, n, N, P), i, j, k with *664    have entrySum := matrixSum.entry at R, n, N, P, k, j with *665    rw [weightN, weightP, weightSum, entrySum]666    ring667  have linear := finiteRingSum.linear at n, R.carrier, R.add, R.zero, R.neg,668    R.mul, R.one, matrixProductWeights(n, K, M, N, i, j),669    matrixProductWeights(n, K, M, P, i, j),670    matrixProductWeights(n, K, M, matrixSum(R, n, N, P), i, j), R[1], R[1] with *671  have closedN := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,672    R.mul, R.one, matrixProductWeights(n, K, M, N, i, j) with *673  have closedP := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,674    R.mul, R.one, matrixProductWeights(n, K, M, P, i, j) with *675  have entryL := matrixProduct.entry_sum at R, n, M, matrixSum(R, n, N, P), i, j with *676  have entryN := matrixProduct.entry_sum at R, n, M, N, i, j with *677  have entryP := matrixProduct.entry_sum at R, n, M, P, i, j with *678  have entryR := matrixSum.entry at R, n, matrixProduct(R, n, M, N),679    matrixProduct(R, n, M, P), i, j with *680  rw [entryL, entryR, entryN, entryP, linear]681  ring682683end MultiplicativeLaws684685-- The triple products behind associativity, as a double array over n × n.686defunique assocWeightValue (R : Set, n : Nat, M N P i j q : Set) (a ∈ Ring.carrier(R)) :=687  ∃ k ∈ n, ∃ l ∈ n, q = (k, l) ∧688    a = call2(Ring.mul(R), M[i, l], call2(Ring.mul(R), N[l, k], P[k, j]))689requires comm : CommRing(R)690requires matrixM : M ∈ squareMatrices(R, n)691requires matrixN : N ∈ squareMatrices(R, n)692requires matrixP : P ∈ squareMatrices(R, n)693requires row : i ∈ n694requires column : j ∈ n695requires pair : q ∈ n × n696proof697  obtain ⟨bound, k, hk, l, hl, shape⟩ := product.membership.forward at698    n, n, q with *699  have entryM := squareMatrices.entry at R, n, M, i, l with *700  have entryN := squareMatrices.entry at R, n, N, l, k with *701  have entryP := squareMatrices.entry at R, n, P, k, j with *702  have inner : N[l, k] * P[k, j] ∈ R := Ring.mul_mem with *703  have value : M[i, l] * (N[l, k] * P[k, j]) ∈ R := Ring.mul_mem with *704  refine ⟨M[i, l] * (N[l, k] * P[k, j]), value, k, hk, l, hl, shape, rfl⟩705uniqueness706  intros u hu first v hv second707  obtain ⟨k, hk, l, hl, shapeU, valueU⟩ := first708  obtain ⟨a, ha, b, hb, shapeV, valueV⟩ := second709  have equal : (k, l) = (a, b)710    cc711  have coordinates := orderedPair.injective at k, l, a, b with equal712  cc713714defgraph assocWeights (R : Set, n : Nat, M N P i j : Set) (q ∈ n × n) : Ring.carrier(R) :=715  assocWeightValue(R, n, M, N, P, i, j, q)716requires comm : CommRing(R)717requires matrixM : M ∈ squareMatrices(R, n)718requires matrixN : N ∈ squareMatrices(R, n)719requires matrixP : P ∈ squareMatrices(R, n)720requires row : i ∈ n721requires column : j ∈ n722proof723  have selected := assocWeightValue.selected at R, n, M, N, P, i, j, q with *724  exact selected.left725726theorem assocWeights.pair (R : Set, n : Nat, M N P i j k l : Set)727  requires comm : CommRing(R)728  requires matrixM : M ∈ squareMatrices(R, n)729  requires matrixN : N ∈ squareMatrices(R, n)730  requires matrixP : P ∈ squareMatrices(R, n)731  requires row : i ∈ n732  requires column : j ∈ n733  requires hk : k ∈ n734  requires hl : l ∈ n735  shows assocWeights(R, n, M, N, P, i, j)((k, l)) = M[i, l] * (N[l, k] * P[k, j])736proof737  have pair := product.pair at k, l, n, n with *738  have selected := assocWeightValue.selected at R, n, M, N, P, i, j, (k, l) with *739  obtain ⟨a, ha, b, hb, shape, result⟩ := selected.right740  have coordinates := orderedPair.injective with shape741  have value := assocWeights.value at R, n, M, N, P, i, j, (k, l) with *742  cc743744section Associativity745variable (R : Set) (n : Nat)746hypothesis comm : CommRing(R)747notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)748749theorem matrixProduct.assoc (M N P : Set)750  requires matrixM : M ∈ squareMatrices(R, n)751  requires matrixN : N ∈ squareMatrices(R, n)752  requires matrixP : P ∈ squareMatrices(R, n)753  shows matrixProduct(R, n, matrixProduct(R, n, M, N), P) =754    matrixProduct(R, n, M, matrixProduct(R, n, N, P))755proof756  have parts := CommRing.parts with comm757  have productMN := matrixProduct.matrix at R, n, M, N with *758  have productNP := matrixProduct.matrix at R, n, N, P with *759  have left := matrixProduct.matrix at R, n, matrixProduct(R, n, M, N), P with *760  have right := matrixProduct.matrix at R, n, M, matrixProduct(R, n, N, P) with *761  have shapeM := squareMatrices.membership.forward with matrixM762  have shapeN := squareMatrices.membership.forward with matrixN763  have shapeP := squareMatrices.membership.forward with matrixP764  have shapeMN := squareMatrices.membership.forward with productMN765  have shapeNP := squareMatrices.membership.forward with productNP766  have finite := Finite.natural at n767  apply squareMatrices.ext with left, right768  intros i hi j hj769  have array := assocWeights.function at R, n, M, N, P, i, j with *770  have transposed := transposedMatrix.function at n, n, R.carrier,771    assocWeights(R, n, M, N, P, i, j) with *772  have rowsL := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,773    R.mul, R.one, assocWeights(R, n, M, N, P, i, j) with *774  have rowsR := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,775    R.mul, R.one, transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)) with *776  have weightsL := matrixProductWeights.function at n, R.carrier, R.add, R.zero,777    R.neg, R.mul, R.one, matrixProduct(R, n, M, N), P, i, j with *778  have weightsR := matrixProductWeights.function at n, R.carrier, R.add, R.zero,779    R.neg, R.mul, R.one, M, matrixProduct(R, n, N, P), i, j with *780  have leftRows : ∀ k ∈ n, matrixProductWeights(n, K, matrixProduct(R, n, M, N), P, i, j)(k) =781      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, assocWeights(R, n, M, N, P, i, j))(k)782    intros k hk783    have entryP := squareMatrices.entry at R, n, P, k, j with *784    have rowWeights := finiteRowWeights.function at n, n, R.carrier,785      assocWeights(R, n, M, N, P, i, j), k with *786    have inner := matrixProductWeights.function at n, R.carrier, R.add, R.zero,787      R.neg, R.mul, R.one, M, N, i, k with *788    have scaled : ∀ l ∈ n, finiteRowWeights(n, n, Ring.carrier(R), assocWeights(R, n, M, N, P, i, j), k)(l) =789        P[k, j] * matrixProductWeights(n, K, M, N, i, k)(l)790      intros l hl791      have entryM := squareMatrices.entry at R, n, M, i, l with *792      have entryN := squareMatrices.entry at R, n, N, l, k with *793      have rowWeight := finiteRowWeights.value at n, n, R.carrier,794        assocWeights(R, n, M, N, P, i, j), k, l with *795      have cell := assocWeights.pair at R, n, M, N, P, i, j, k, l with *796      have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,797        R.neg, R.mul, R.one, M, N, i, k, l with *798      rw [rowWeight, cell, weight]799      ring800    have scale := finiteRingSum.scale_eq at n, R.carrier, R.add, R.zero, R.neg,801      R.mul, R.one, matrixProductWeights(n, K, M, N, i, k),802      finiteRowWeights(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j), k), P[k, j] with *803    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,804      R.mul, R.one, assocWeights(R, n, M, N, P, i, j), k with *805    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,806      R.neg, R.mul, R.one, matrixProduct(R, n, M, N), P, i, j, k with *807    have entryMN := matrixProduct.entry_sum at R, n, M, N, i, k with *808    have closed := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,809      R.mul, R.one, matrixProductWeights(n, K, M, N, i, k) with *810    rw [weight, rowSum, scale, entryMN]811    ring812  have rightRows : ∀ l ∈ n, matrixProductWeights(n, K, M, matrixProduct(R, n, N, P), i, j)(l) =813      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, transposedMatrix(n, n, Ring.carrier(R), assocWeights(R, n, M, N, P, i, j)))(l)814    intros l hl815    have entryM := squareMatrices.entry at R, n, M, i, l with *816    have rowWeights := finiteRowWeights.function at n, n, R.carrier,817      transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)), l with *818    have inner := matrixProductWeights.function at n, R.carrier, R.add, R.zero,819      R.neg, R.mul, R.one, N, P, l, j with *820    have scaled : ∀ k ∈ n, finiteRowWeights(n, n, Ring.carrier(R), transposedMatrix(n, n, Ring.carrier(R), assocWeights(R, n, M, N, P, i, j)), l)(k) =821        M[i, l] * matrixProductWeights(n, K, N, P, l, j)(k)822      intros k hk823      have entryN := squareMatrices.entry at R, n, N, l, k with *824      have entryP := squareMatrices.entry at R, n, P, k, j with *825      have rowWeight := finiteRowWeights.value at n, n, R.carrier,826        transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)), l, k with *827      have swap := transposedMatrix.pair at n, n, R.carrier,828        assocWeights(R, n, M, N, P, i, j), k, l with *829      have cell := assocWeights.pair at R, n, M, N, P, i, j, k, l with *830      have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,831        R.neg, R.mul, R.one, N, P, l, j, k with *832      rw [rowWeight, swap, cell, weight]833      ring834    have scale := finiteRingSum.scale_eq at n, R.carrier, R.add, R.zero, R.neg,835      R.mul, R.one, matrixProductWeights(n, K, N, P, l, j),836      finiteRowWeights(n, n, R.carrier, transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)), l), M[i, l] with *837    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,838      R.mul, R.one, transposedMatrix(n, n, R.carrier, assocWeights(R, n, M, N, P, i, j)), l with *839    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,840      R.neg, R.mul, R.one, M, matrixProduct(R, n, N, P), i, j, l with *841    have entryNP := matrixProduct.entry_sum at R, n, N, P, l, j with *842    rw [weight, rowSum, scale, entryNP]843    rfl844  have sameL := finiteRingSum.congr with leftRows845  have sameR := finiteRingSum.congr with rightRows846  have interchange := finiteDoubleSum.interchange at n, n, R.carrier, R.add, R.zero,847    R.neg, R.mul, R.one, assocWeights(R, n, M, N, P, i, j) with *848  have entryL := matrixProduct.entry_sum at R, n, matrixProduct(R, n, M, N), P, i, j with *849  have entryR := matrixProduct.entry_sum at R, n, M, matrixProduct(R, n, N, P), i, j with *850  unfold finiteDoubleSum at interchange851  cc852853end Associativity854855-- The ring laws over separate pieces, then the ring instance.856section Instances857variable (R : Set) (n : Nat)858hypothesis comm : CommRing(R)859notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)860861theorem matrixRing.engine862  shows IsRing(squareMatrices(R, n), matrixAddition(R, n), zeroMatrix(R, n),863    matrixNegation(R, n), matrixMultiplication(R, n), oneMatrix(R, n))864proof865  have addMagma : IsMagma(squareMatrices(R, n), matrixAddition(R, n))866    exact matrixAddition.function at R, n with *867  have mulMagma : IsMagma(squareMatrices(R, n), matrixMultiplication(R, n))868    exact matrixMultiplication.function at R, n with *869  have negF := matrixNegation.function at R, n with *870  have zero := zeroMatrix.matrix at R, n with *871  have one := oneMatrix.matrix at R, n with *872  have addAssoc : Associative(squareMatrices(R, n), matrixAddition(R, n))873    intros M hM N hN P hP874    have sumMN := matrixSum.matrix at R, n, M, N with *875    have sumNP := matrixSum.matrix at R, n, N, P with *876    have first := matrixAddition.apply at R, n, M, N with *877    have second := matrixAddition.apply at R, n, matrixSum(R, n, M, N), P with *878    have third := matrixAddition.apply at R, n, N, P with *879    have fourth := matrixAddition.apply at R, n, M, matrixSum(R, n, N, P) with *880    have assoc := matrixSum.assoc at R, n, M, N, P with *881    cc882  have addComm : Commutative(squareMatrices(R, n), matrixAddition(R, n))883    intros M hM N hN884    have first := matrixAddition.apply at R, n, M, N with *885    have second := matrixAddition.apply at R, n, N, M with *886    have swap := matrixSum.comm at R, n, M, N with *887    cc888  have addUnit : Identity(squareMatrices(R, n), matrixAddition(R, n), zeroMatrix(R, n))889    refine ⟨zero, ?_⟩890    intros M hM891    have first := matrixAddition.apply at R, n, zeroMatrix(R, n), M with *892    have second := matrixAddition.apply at R, n, M, zeroMatrix(R, n) with *893    have left := matrixSum.zero_left at R, n, M with *894    have right := matrixSum.zero_right at R, n, M with *895    constructor896    . cc897    . cc898  have addInverse : Inverse(squareMatrices(R, n), matrixAddition(R, n),899      zeroMatrix(R, n), matrixNegation(R, n))900    refine ⟨negF, ?_⟩901    intros M hM902    have negative := matrixNegative.matrix at R, n, M with *903    have value := matrixNegation.value at R, n, M with *904    have first := matrixAddition.apply at R, n, matrixNegative(R, n, M), M with *905    have second := matrixAddition.apply at R, n, M, matrixNegative(R, n, M) with *906    have left := matrixSum.neg_left at R, n, M with *907    have right := matrixSum.neg_right at R, n, M with *908    constructor909    . cc910    . cc911  have mulAssoc : Associative(squareMatrices(R, n), matrixMultiplication(R, n))912    intros M hM N hN P hP913    have productMN := matrixProduct.matrix at R, n, M, N with *914    have productNP := matrixProduct.matrix at R, n, N, P with *915    have first := matrixMultiplication.apply at R, n, M, N with *916    have second := matrixMultiplication.apply at R, n, matrixProduct(R, n, M, N), P with *917    have third := matrixMultiplication.apply at R, n, N, P with *918    have fourth := matrixMultiplication.apply at R, n, M, matrixProduct(R, n, N, P) with *919    have assoc := matrixProduct.assoc at R, n, M, N, P with *920    cc921  have mulUnit : Identity(squareMatrices(R, n), matrixMultiplication(R, n), oneMatrix(R, n))922    refine ⟨one, ?_⟩923    intros M hM924    have first := matrixMultiplication.apply at R, n, oneMatrix(R, n), M with *925    have second := matrixMultiplication.apply at R, n, M, oneMatrix(R, n) with *926    have left := matrixProduct.one_left at R, n, M with *927    have right := matrixProduct.one_right at R, n, M with *928    constructor929    . cc930    . cc931  have distributive : Distributive(squareMatrices(R, n), matrixAddition(R, n),932      matrixMultiplication(R, n))933    intros M hM N hN P hP934    have sumNP := matrixSum.matrix at R, n, N, P with *935    have sumMN := matrixSum.matrix at R, n, M, N with *936    have productMN := matrixProduct.matrix at R, n, M, N with *937    have productMP := matrixProduct.matrix at R, n, M, P with *938    have productNP := matrixProduct.matrix at R, n, N, P with *939    have addNP := matrixAddition.apply at R, n, N, P with *940    have addMN := matrixAddition.apply at R, n, M, N with *941    have mulLeft := matrixMultiplication.apply at R, n, M, matrixSum(R, n, N, P) with *942    have mulRight := matrixMultiplication.apply at R, n, matrixSum(R, n, M, N), P with *943    have mulMN := matrixMultiplication.apply at R, n, M, N with *944    have mulMP := matrixMultiplication.apply at R, n, M, P with *945    have mulNP := matrixMultiplication.apply at R, n, N, P with *946    have addLeft := matrixAddition.apply at R, n, matrixProduct(R, n, M, N),947      matrixProduct(R, n, M, P) with *948    have addRight := matrixAddition.apply at R, n, matrixProduct(R, n, M, P),949      matrixProduct(R, n, N, P) with *950    have left := matrixProduct.sum_right at R, n, M, N, P with *951    have right := matrixProduct.sum_left at R, n, M, N, P with *952    constructor953    . cc954    . cc955  unfold IsRing956  simp [IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]957958instance matrixRing.ring959  shows Ring(matrixRing(R, n))960proof961  have engine := matrixRing.engine at R, n with comm962  unfold matrixRing963  exact Ring.of_parts with engine964965end Instances966967-- A matrix as a guard: (M : R ^ n × n) is Matrix(M, R, n, n), membership968-- in the matrix ring, opened to M ∈ Ring.carrier(matrixRing(R, n))969-- wherever local evidence is consulted, so (M N : R ^ n × n) carry970-- M + N, M * N, -M, and the constants matrixRing(R, n)[0] and971-- matrixRing(R, n)[1]; det(M) and adj(M) are the determinant and the972-- adjugate over R. The shape m × n is written for the guard's sake: this973-- layer has square matrices only, and Matrix(M, R, m, n) requires m = n.974predicate Matrix (M R m n : Set) := m = n ∧ M ∈ Ring.carrier(matrixRing(R, n))975notation guard "_ : _ ^ _ × _" => Matrix976notation function "det(M)" => determinant(n, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), M) via hypothesis Matrix(M, R, m, n)977notation function "adj(M)" => adjugate(n, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), M) via hypothesis Matrix(M, R, m, n)978notation infixl 60 "+" => call2(Ring.add(matrixRing(R, n)), _, _) via hypothesis Matrix(M, R, m, n) for Ring.carrier(matrixRing(R, n))979notation infixl 70 "*" => call2(Ring.mul(matrixRing(R, n)), _, _) via hypothesis Matrix(M, R, m, n) for Ring.carrier(matrixRing(R, n))980notation prefix 75 "-" => apply(Ring.neg(matrixRing(R, n)), _) via hypothesis Matrix(M, R, m, n) for Ring.carrier(matrixRing(R, n))981notation infixl 60 "-" => Ring.sub(matrixRing(R, n), _, _) via hypothesis Matrix(M, R, m, n) for Ring.carrier(matrixRing(R, n))982983theorem Matrix.of_mem (M R n : Set)984  requires member : M ∈ Ring.carrier(matrixRing(R, n))985  shows M : R ^ n × n986proof987  unfold Matrix988  exact ⟨rfl, member⟩989990theorem Matrix.mem_ring (M R n : Set)991  requires matrix : M : R ^ n × n992  shows M ∈ Ring.carrier(matrixRing(R, n))993proof994  assumption995996theorem Matrix.square (M R n : Set)997  requires matrix : M : R ^ n × n998  shows M ∈ squareMatrices(R, n)999proof1000  have member : M ∈ Ring.carrier(matrixRing(R, n)) by assumption1001  rw matrixRing.carrierOf at member1002  exact member10031004theorem Matrix.of_square (M R n : Set)1005  requires matrix : M ∈ squareMatrices(R, n)1006  shows M : R ^ n × n1007proof1008  unfold Matrix1009  refine ⟨rfl, ?_⟩1010  rw matrixRing.carrierOf1011  exact matrix10121013theorem Matrix.function (M R n : Set)1014  requires matrix : M : R ^ n × n1015  shows M : n × n → Ring.carrier(R)1016proof1017  have square := Matrix.square with matrix1018  exact squareMatrices.function with square10191020theorem Matrix.of_function (M R n : Set)1021  requires function : M : n × n → Ring.carrier(R)1022  shows M : R ^ n × n1023proof1024  have square := squareMatrices.of_function with function1025  exact Matrix.of_square with square10261027theorem Matrix.entry (M R n i j : Set)1028  requires matrix : M : R ^ n × n1029  requires row : i ∈ n1030  requires column : j ∈ n1031  shows M[i, j] ∈ Ring.carrier(R)1032proof1033  have function := Matrix.function with matrix1034  have pair := product.pair at i, j, n, n with *1035  exact FunctionBetween.apply_closed with function, pair10361037theorem Matrix.ext (M N R n : Set)1038  requires matrixM : M : R ^ n × n1039  requires matrixN : N : R ^ n × n1040  requires entries : ∀ i ∈ n, ∀ j ∈ n, M[i, j] = N[i, j]1041  shows M = N1042proof1043  have functionM := Matrix.function with matrixM1044  have functionN := Matrix.function with matrixN1045  have values : ∀ p ∈ n × n, M(p) = N(p)1046    intros p hp1047    obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with hp1048    rw shape1049    exact entries with i, hi, j, hj1050  exact FunctionBetween.ext with functionM, functionN, values1051