Grace/Cumulus/Algebra/Ring/MatrixEntries.g17

Open in Workbench Download source

Imports

MatrixRing

Declarations

Source

1-- Entries of the bundled matrix operations: under CommRing(R) a binder2-- (M : R ^ n × n) is a square matrix, its elements carry M + N,3-- M * N, and -M, the constants are matrixRing(R, n)[0] and4-- matrixRing(R, n)[1], and each operation is read entry by entry; the5-- determinant and the adjugate of a square matrix are det(M) and adj(M)6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Ring.MatrixEntries12import MatrixRing1314section Entries15variable (R : Set) (n : Nat)16hypothesis comm : CommRing(R)1718theorem matrixRing.add_entry (M N : R ^ n × n) (i j : Set)19  requires row : i ∈ n20  requires column : j ∈ n21  shows (M + N)[i, j] = M[i, j] + N[i, j]22proof23  have matrixM := Matrix.square at M, R, n with assumption24  have matrixN := Matrix.square at N, R, n with assumption25  have sum := matrixAddition.apply at R, n, M, N with *26  have entry := matrixSum.entry at R, n, M, N, i, j with *27  rw [matrixRing.addOf, sum, entry]28  rfl2930theorem matrixRing.mul_entry (M N : R ^ n × n) (i j : Set)31  requires row : i ∈ n32  requires column : j ∈ n33  shows (M * N)[i, j] = matrixProductEntry(n, Ring.carrier(R), Ring.add(R),34    Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), M, N, i, j)35proof36  have matrixM := Matrix.square at M, R, n with assumption37  have matrixN := Matrix.square at N, R, n with assumption38  have product := matrixMultiplication.apply at R, n, M, N with *39  have entry := matrixProduct.entry at R, n, M, N, i, j with *40  rw [matrixRing.mulOf, product, entry]41  rfl4243theorem matrixRing.neg_entry (M : R ^ n × n) (i j : Set)44  requires row : i ∈ n45  requires column : j ∈ n46  shows (-M)[i, j] = -M[i, j]47proof48  have matrix := Matrix.square at M, R, n with assumption49  have negation := matrixNegation.value at R, n, M with *50  have entry := matrixNegative.entry at R, n, M, i, j with *51  rw [matrixRing.negOf, negation, entry]52  rfl5354theorem matrixRing.zero_entry (i j : Set)55  requires row : i ∈ n56  requires column : j ∈ n57  shows matrixRing(R, n)[0][i, j] = R[0]58proof59  have entry := zeroMatrix.entry at R, n, i, j with *60  rw [matrixRing.zeroOf, entry]61  rfl6263theorem matrixRing.one_entry (i j : Set)64  requires row : i ∈ n65  requires column : j ∈ n66  shows matrixRing(R, n)[1][i, j] = singleValue(R.carrier, R.zero, R.one, j, i)67proof68  have entry := oneMatrix.entry at R, n, i, j with *69  rw [matrixRing.oneOf, entry]70  rfl7172theorem matrixRing.ext (M N : R ^ n × n)73  requires entries : ∀ i ∈ n, ∀ j ∈ n, M[i, j] = N[i, j]74  shows M = N75proof76  have matrixM := Matrix.square at M, R, n with assumption77  have matrixN := Matrix.square at N, R, n with assumption78  exact squareMatrices.ext with matrixM, matrixN, entries7980-- The determinant and the adjugate of a square matrix.81theorem Matrix.det_mem (M : R ^ n × n)82  shows det(M) ∈ R83proof84  have parts := CommRing.parts with comm85  have matrix := Matrix.square at M, R, n with assumption86  have shape := squareMatrices.membership.forward with matrix87  exact determinant.closed with parts, shape8889theorem Matrix.adj_matrix (M : R ^ n × n)90  shows adj(M) : R ^ n × n91proof92  have parts := CommRing.parts with comm93  have matrix := Matrix.square at M, R, n with assumption94  have shape := squareMatrices.membership.forward with matrix95  have finite := Finite.natural at n96  have adjugate := adjugate.matrix at n, R.carrier, R.add, R.zero, R.neg,97    R.mul, R.one, M with *98  have square := squareMatrices.membership.backward with adjugate99  exact Matrix.of_square with square100101theorem Matrix.adj_entry (M : R ^ n × n) (i j : Set)102  requires row : i ∈ n103  requires column : j ∈ n104  shows adj(M)[i, j] = cofactorRow(n, R.carrier, R.add, R.zero, R.neg, R.mul,105    R.one, M, j)(i)106proof107  have parts := CommRing.parts with comm108  have matrix := Matrix.square at M, R, n with assumption109  have shape := squareMatrices.membership.forward with matrix110  have finite := Finite.natural at n111  exact adjugate.entry with *112113end Entries114