Reference · Matrices

rainbow.math.linear.matrix.equivalence

Matricessrc/rainbow/math/linear/matrix/equivalence.clj1 definitions, 4 theorems

Length-sensitive, row-wise equivalence for native finite matrices. matrix/equivalent left right Matrices are equivalent exactly when they have the same number of rows and corresponding rows are vector/equivalent. Reflexivity and symmetry are proved structurally. Matrix-vector multiplication then respects matrix equivalence, and a final theorem composes matrix-side and input-vector congruence. Native and axiom-free on D63.

Depends onmath.finite.matrix

matrix/equivalent :
  (x₁ x₂ : List (List ℚ))
  → Prop

matrix/equivalent-reflexive :
  (rows : List (List ℚ))
  → matrix/equivalent rows rows

matrix/equivalent-symmetric :
  (left right : List (List ℚ)) (same : matrix/equivalent left right)
  → matrix/equivalent right left

matrix/vector-multiply-respects-matrix-equivalence :
  (left right : List (List ℚ)) (values : List ℚ) (same : matrix/equivalent left right)
  → vector/equivalent (matrix/vector-multiply left values) (matrix/vector-multiply right values)

matrix/vector-multiply-respects-both-equivalences :
  (left-rows right-rows : List (List ℚ)) (left-values right-values : List ℚ)
  (rows-same : matrix/equivalent left-rows right-rows)
  (values-same : vector/equivalent left-values right-values)
  → vector/equivalent (multiply₁) (multiply)
  where multiply := matrix/vector-multiply right-rows right-values
  where multiply₁ := matrix/vector-multiply left-rows left-values