Reference · Vectors

rainbow.math.linear.vector.additive-units

Vectorssrc/rainbow/math/linear/vector/additive_units.clj1 definitions, 5 theorems

Shape-preserving zero and additive-unit laws for native finite vectors. Since vector/add is a truncating zip, the empty vector cannot be a global additive identity. vector/zero-like instead maps signed/zero over an input, preserving exactly its dimension. It is a two-sided identity for that input, and adding either orientation of the input and its negation is equivalent to zero-like. Native and axiom-free on D63.

Depends onmath.rational.signed.unit-laws

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

vector/add-zero-like-right :
  (values : List ℚ)
  → vector/equivalent (add) values
  where add := vector/add values (vector/zero-like values)

vector/add-zero-like-left :
  (values : List ℚ)
  → vector/equivalent (add) values
  where add := vector/add (vector/zero-like values) values

vector/subtract-self-equivalent-zero-like :
  (values : List ℚ)
  → vector/equivalent (vector/subtract values values) (vector/zero-like values)

vector/add-negate-right-equivalent-zero-like :
  (values : List ℚ)
  → vector/equivalent (add) (vector/zero-like values)
  where add := vector/add values (vector/negate values)

vector/add-negate-left-equivalent-zero-like :
  (values : List ℚ)
  → vector/equivalent (add) (vector/zero-like values)
  where add := vector/add (vector/negate values) values