Reference · Matrices

rainbow.math.linear.matrix.additive-group

Matricessrc/rainbow/math/linear/matrix/additive_group.clj3 definitions, 8 theorems

Shaped zero, negation, subtraction, and inverse laws for matrices. The three operations map existing vector operations over rows (with subtraction defined by addition and negation). Zero and negation preserve complete matrix shape; same-shaped subtraction preserves both operand shapes. Matrix addition has shaped identities and inverses, including self-subtraction to the shaped zero matrix. Native and axiom-free on D63.

Depends onmath.linear.matrix.add-algebra

matrix/zero-like :
  (x₁ : List (List ℚ))
  → List (List ℚ)

matrix/negate :
  (x₁ : List (List ℚ))
  → List (List ℚ)

matrix/subtract :
  (x₁ x₂ : List (List ℚ))
  → List (List ℚ)

matrix/zero-like-preserves-same-shape :
  (rows : List (List ℚ))
  → matrix/same-shape (matrix/zero-like rows) rows

matrix/negate-preserves-same-shape :
  (rows : List (List ℚ))
  → matrix/same-shape (matrix/negate rows) rows

matrix/subtract-preserves-shape :
  (left right : List (List ℚ)) (same : matrix/same-shape left right)
  → proposition/conjunction (shape₁) (shape)
  where shape := matrix/same-shape (matrix/subtract left right) right
  where shape₁ := matrix/same-shape (matrix/subtract left right) left

matrix/add-zero-like-right :
  (rows : List (List ℚ))
  → matrix/equivalent (matrix/add rows (matrix/zero-like rows)) rows

matrix/add-zero-like-left :
  (rows : List (List ℚ))
  → matrix/equivalent (matrix/add (matrix/zero-like rows) rows) rows

matrix/add-negate-right-equivalent-zero-like :
  (rows : List (List ℚ))
  → matrix/equivalent (matrix/add rows (matrix/negate rows)) (matrix/zero-like rows)

matrix/add-negate-left-equivalent-zero-like :
  (rows : List (List ℚ))
  → matrix/equivalent (matrix/add (matrix/negate rows) rows) (matrix/zero-like rows)

matrix/subtract-self-equivalent-zero-like :
  (rows : List (List ℚ))
  → matrix/equivalent (matrix/subtract rows rows) (matrix/zero-like rows)