Reference · Vectors

rainbow.math.linear.vector.shape-cancellation

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

Shape equality and sound cancellation for truncating vector arithmetic. Native vector/add truncates to the shorter list, so cancellation is false without a dimension hypothesis. vector/same-shape compares the corresponding zero-like vectors and therefore records equal dimension without inspecting components. Under that hypothesis both right-cancellation orientations hold: (left - right) + right ~ left (left + right) - right ~ left Native and axiom-free on D63.

Depends onmath.linear.vector.additive-units

vector/same-shape :
  (x₁ x₂ : List ℚ)
  → Prop

vector/same-shape-reflexive :
  (values : List ℚ)
  → vector/same-shape values values

vector/same-shape-symmetric :
  (left right : List ℚ) (same : vector/same-shape left right)
  → vector/same-shape right left

vector/same-shape-transitive :
  (left middle right : List ℚ) (left-middle : vector/same-shape left middle)
  (middle-right : vector/same-shape middle right)
  → vector/same-shape left right

vector/subtract-add-right-cancel :
  (left right : List ℚ) (same : vector/same-shape left right)
  → vector/equivalent (add) left
  where add := vector/add (vector/subtract left right) right

vector/add-subtract-right-cancel :
  (left right : List ℚ) (same : vector/same-shape left right)
  → vector/equivalent (subtract) left
  where subtract := vector/subtract (vector/add left right) right