-- Entries of the bundled matrix operations: under CommRing(R) a binder
-- (M : R ^ n × n) is a square matrix, its elements carry M + N,
-- M * N, and -M, the constants are matrixRing(R, n)[0] and
-- matrixRing(R, n)[1], and each operation is read entry by entry; the
-- determinant and the adjugate of a square matrix are det(M) and adj(M)
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Ring.MatrixEntries
import MatrixRing

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

theorem matrixRing.add_entry (M N : R ^ n × n) (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows (M + N)[i, j] = M[i, j] + N[i, j]
proof
  have matrixM := Matrix.square at M, R, n with assumption
  have matrixN := Matrix.square at N, R, n with assumption
  have sum := matrixAddition.apply at R, n, M, N with *
  have entry := matrixSum.entry at R, n, M, N, i, j with *
  rw [matrixRing.addOf, sum, entry]
  rfl

theorem matrixRing.mul_entry (M N : R ^ n × n) (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows (M * N)[i, j] = matrixProductEntry(n, Ring.carrier(R), Ring.add(R),
    Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), M, N, i, j)
proof
  have matrixM := Matrix.square at M, R, n with assumption
  have matrixN := Matrix.square at N, R, n with assumption
  have product := matrixMultiplication.apply at R, n, M, N with *
  have entry := matrixProduct.entry at R, n, M, N, i, j with *
  rw [matrixRing.mulOf, product, entry]
  rfl

theorem matrixRing.neg_entry (M : R ^ n × n) (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows (-M)[i, j] = -M[i, j]
proof
  have matrix := Matrix.square at M, R, n with assumption
  have negation := matrixNegation.value at R, n, M with *
  have entry := matrixNegative.entry at R, n, M, i, j with *
  rw [matrixRing.negOf, negation, entry]
  rfl

theorem matrixRing.zero_entry (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows matrixRing(R, n)[0][i, j] = R[0]
proof
  have entry := zeroMatrix.entry at R, n, i, j with *
  rw [matrixRing.zeroOf, entry]
  rfl

theorem matrixRing.one_entry (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows matrixRing(R, n)[1][i, j] = singleValue(R.carrier, R.zero, R.one, j, i)
proof
  have entry := oneMatrix.entry at R, n, i, j with *
  rw [matrixRing.oneOf, entry]
  rfl

theorem matrixRing.ext (M N : R ^ n × n)
  requires entries : ∀ i ∈ n, ∀ j ∈ n, M[i, j] = N[i, j]
  shows M = N
proof
  have matrixM := Matrix.square at M, R, n with assumption
  have matrixN := Matrix.square at N, R, n with assumption
  exact squareMatrices.ext with matrixM, matrixN, entries

-- The determinant and the adjugate of a square matrix.
theorem Matrix.det_mem (M : R ^ n × n)
  shows det(M) ∈ R
proof
  have parts := CommRing.parts with comm
  have matrix := Matrix.square at M, R, n with assumption
  have shape := squareMatrices.membership.forward with matrix
  exact determinant.closed with parts, shape

theorem Matrix.adj_matrix (M : R ^ n × n)
  shows adj(M) : R ^ n × n
proof
  have parts := CommRing.parts with comm
  have matrix := Matrix.square at M, R, n with assumption
  have shape := squareMatrices.membership.forward with matrix
  have finite := Finite.natural at n
  have adjugate := adjugate.matrix at n, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, M with *
  have square := squareMatrices.membership.backward with adjugate
  exact Matrix.of_square with square

theorem Matrix.adj_entry (M : R ^ n × n) (i j : Set)
  requires row : i ∈ n
  requires column : j ∈ n
  shows adj(M)[i, j] = cofactorRow(n, R.carrier, R.add, R.zero, R.neg, R.mul,
    R.one, M, j)(i)
proof
  have parts := CommRing.parts with comm
  have matrix := Matrix.square at M, R, n with assumption
  have shape := squareMatrices.membership.forward with matrix
  have finite := Finite.natural at n
  exact adjugate.entry with *

end Entries