hex

11.4. Entry, row, and column lemmas🔗

Every operation above carries a complete set of description lemmas: an entry lemma getElem_… fixing M[i][j], and row_…/col_… lemmas fixing a whole row or column. This grid is kept total — zero, Hex.Matrix.identity, Hex.Matrix.transpose, Hex.Matrix.mulVec, Hex.Matrix.vecMul, Hex.Matrix.mul, Hex.Matrix.gramMatrix, Hex.Matrix.principalSubmatrix, and every elementary operation each carry all three — so a proof can rewrite in whichever shape it needs. The lemmas below are representative rather than exhaustive.

Transpose exchanges rows and columns, and is an involution:

🔗theorem
Hex.Matrix.getElem_transpose.{u} {R : Type u} {n m : ℕ}
  (M : Hex.Matrix R n m) (i : Fin m) (j : Fin n) :
  M.transpose[i][j] = M[j][i]
Hex.Matrix.getElem_transpose.{u}
  {R : Type u} {n m : ℕ}
  (M : Hex.Matrix R n m) (i : Fin m)
  (j : Fin n) :
  M.transpose[i][j] = M[j][i]

Entry access for the transpose of a dense matrix.

🔗theorem
Hex.Matrix.row_transpose.{u} {R : Type u} {n m : ℕ}
  (M : Hex.Matrix R n m) (j : Fin m) : M.transpose.row j = M.col j
Hex.Matrix.row_transpose.{u} {R : Type u}
  {n m : ℕ} (M : Hex.Matrix R n m)
  (j : Fin m) :
  M.transpose.row j = M.col j

The j-th row of transpose M is the j-th column of M.

🔗theorem
Hex.Matrix.transpose_transpose.{u} {R : Type u} {n m : ℕ}
  (M : Hex.Matrix R n m) : M.transpose.transpose = M
Hex.Matrix.transpose_transpose.{u}
  {R : Type u} {n m : ℕ}
  (M : Hex.Matrix R n m) :
  M.transpose.transpose = M

Transposing a dense matrix twice returns the original matrix.

Every product entry is a dot product: matrix-vector, vector-matrix, and matrix-matrix multiplication all read off Vector.dotProduct.

🔗theorem
Hex.Matrix.getElem_mulVec.{u} {R : Type u} {n m : ℕ} [Mul R] [Add R]
  [OfNat R 0] (M : Hex.Matrix R n m) (v : Vector R m) (i : Fin n) :
  (M * v)[i] = (M.row i).dotProduct v
Hex.Matrix.getElem_mulVec.{u} {R : Type u}
  {n m : ℕ} [Mul R] [Add R] [OfNat R 0]
  (M : Hex.Matrix R n m) (v : Vector R m)
  (i : Fin n) :
  (M * v)[i] = (M.row i).dotProduct v

Entry characterization for matrix-vector multiplication.

🔗theorem
Hex.Matrix.getElem_vecMul.{u} {R : Type u} {n m : ℕ} [Mul R] [Add R]
  [OfNat R 0] (v : Vector R n) (M : Hex.Matrix R n m) (j : Fin m) :
  (v * M)[j] = (M.col j).dotProduct v
Hex.Matrix.getElem_vecMul.{u} {R : Type u}
  {n m : ℕ} [Mul R] [Add R] [OfNat R 0]
  (v : Vector R n) (M : Hex.Matrix R n m)
  (j : Fin m) :
  (v * M)[j] = (M.col j).dotProduct v

Entry characterization for vector-matrix multiplication.

🔗theorem
Hex.Matrix.getElem_mul.{u} {R : Type u} {n m k : ℕ} [Mul R] [Add R]
  [OfNat R 0] (M : Hex.Matrix R n m) (N : Hex.Matrix R m k) (i : Fin n)
  (j : Fin k) : (M * N)[i][j] = (M.row i).dotProduct (N.col j)
Hex.Matrix.getElem_mul.{u} {R : Type u}
  {n m k : ℕ} [Mul R] [Add R] [OfNat R 0]
  (M : Hex.Matrix R n m)
  (N : Hex.Matrix R m k) (i : Fin n)
  (j : Fin k) :
  (M * N)[i][j] =
    (M.row i).dotProduct (N.col j)

Entry characterization for matrix multiplication.

The identity entries are the Kronecker delta, the identity is a left and right unit, and multiplication is associative:

🔗theorem
Hex.Matrix.getElem_identity.{u} {R : Type u} [OfNat R 0] [OfNat R 1]
  {n : ℕ} (i j : Fin n) :
  (Hex.Matrix.identity n)[i][j] = if i = j then 1 else 0
Hex.Matrix.getElem_identity.{u}
  {R : Type u} [OfNat R 0] [OfNat R 1]
  {n : ℕ} (i j : Fin n) :
  (Hex.Matrix.identity n)[i][j] =
    if i = j then 1 else 0

The identity matrix entry function: (identity n)[i][j] = 1 if i = j, else 0.

🔗theorem
Hex.Matrix.identity_mul.{u_1} {R : Type u_1} {n m : ℕ}
  [Lean.Grind.Ring R] (M : Hex.Matrix R n m) :
  Hex.Matrix.identity n * M = M
Hex.Matrix.identity_mul.{u_1}
  {R : Type u_1} {n m : ℕ}
  [Lean.Grind.Ring R]
  (M : Hex.Matrix R n m) :
  Hex.Matrix.identity n * M = M

Left-multiplication by the identity matrix leaves a matrix unchanged.

🔗theorem
Hex.Matrix.mul_identity.{u_1} {R : Type u_1} {n m : ℕ}
  [Lean.Grind.Ring R] (M : Hex.Matrix R n m) :
  M * Hex.Matrix.identity m = M
Hex.Matrix.mul_identity.{u_1}
  {R : Type u_1} {n m : ℕ}
  [Lean.Grind.Ring R]
  (M : Hex.Matrix R n m) :
  M * Hex.Matrix.identity m = M

Right-multiplication by the identity matrix leaves a matrix unchanged.

🔗theorem
Hex.Matrix.mul_assoc.{u_1} {R : Type u_1} {n m k l : ℕ}
  [Lean.Grind.Ring R] (A : Hex.Matrix R n m) (B : Hex.Matrix R m k)
  (C : Hex.Matrix R k l) : A * B * C = A * (B * C)
Hex.Matrix.mul_assoc.{u_1} {R : Type u_1}
  {n m k l : ℕ} [Lean.Grind.Ring R]
  (A : Hex.Matrix R n m)
  (B : Hex.Matrix R m k)
  (C : Hex.Matrix R k l) :
  A * B * C = A * (B * C)

Matrix multiplication is associative.

The Gram matrix pairs the rows against one another:

🔗theorem
Hex.Matrix.getElem_gramMatrix.{u_1} {R : Type u_1} {n m : ℕ} [Mul R]
  [Add R] [OfNat R 0] (M : Hex.Matrix R n m) (i j : Fin n) :
  M.gramMatrix[i][j] = (M.row i).dotProduct (M.row j)
Hex.Matrix.getElem_gramMatrix.{u_1}
  {R : Type u_1} {n m : ℕ} [Mul R] [Add R]
  [OfNat R 0] (M : Hex.Matrix R n m)
  (i j : Fin n) :
  M.gramMatrix[i][j] =
    (M.row i).dotProduct (M.row j)

Entry characterization for the Gram matrix of the rows of a dense matrix.