Reference · Matrices

rainbow.math.linear.matrix.add-algebra

Matricessrc/rainbow/math/linear/matrix/add_algebra.clj0 definitions, 5 theorems

Commutative, associative, quotient-safe native matrix addition. Because row-wise matrix/add and vector/add both use symmetric truncating zip semantics, commutativity and associativity need no shape premise. Structural congruence in each argument makes the operation well defined over native matrix equivalence. Native and axiom-free on D63.

Depends onmath.linear.matrix.add-right

matrix/add-commutative :
  (left right : List (List ℚ))
  → matrix/equivalent (matrix/add left right) (matrix/add right left)

matrix/add-associative :
  (left middle right : List (List ℚ))
  → matrix/equivalent (add) (add₁)
  where add := matrix/add (matrix/add left middle) right
  where add₁ := matrix/add left (matrix/add middle right)

matrix/add-respects-left-equivalence :
  (left equivalent-left right : List (List ℚ))
  (same : matrix/equivalent left equivalent-left)
  → matrix/equivalent (matrix/add left right) (matrix/add equivalent-left right)

matrix/add-respects-right-equivalence :
  (left right equivalent-right : List (List ℚ))
  (same : matrix/equivalent right equivalent-right)
  → matrix/equivalent (matrix/add left right) (matrix/add left equivalent-right)

matrix/add-respects-equivalence :
  (left equivalent-left right equivalent-right : List (List ℚ))
  (left-same : matrix/equivalent left equivalent-left)
  (right-same : matrix/equivalent right equivalent-right)
  → matrix/equivalent (matrix/add left right) (add)
  where add := matrix/add equivalent-left equivalent-right