Reference · Matrices

rainbow.math.linear.matrix.signed-scale-subtract

Matricessrc/rainbow/math/linear/matrix/signed_scale_subtract.clj0 definitions, 14 theorems

Negation and subtraction laws for signed multiplication and module scaling. Multiplication distributes over subtraction on either side. Via the checked scale-difference/multiplication bridge, negating or subtracting either the factor or value commutes with signed scaling. Structural vector and matrix lifts complete the same laws; value subtraction carries an exact-shape premise because native subtraction zips its two inputs. Native and axiom-free on D63.

Depends onmath.linear.matrix.signed-scale-congruence

signed/multiply-subtract-left :
  (left right factor : ℚ)
  → (left - right) · factor = left · factor - right · factor

signed/multiply-subtract-right :
  (factor left right : ℚ)
  → factor · (left - right) = factor · left - factor · right

signed/scale-difference-negate-factor :
  (factor value : ℚ)
  → signed/scale (signed/positive (signed/negate factor)) value - signed/scale (signed/negative (signed/negate factor)) value = signed/negate (signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value)

signed/scale-difference-negate-value :
  (factor value : ℚ)
  → signed/scale (signed/positive factor) (signed/negate value) - signed/scale (signed/negative factor) (signed/negate value) = signed/negate (signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value)

signed/scale-difference-subtract-factor :
  (left right value : ℚ)
  → signed/scale (signed/positive (left - right)) value - signed/scale (signed/negative (left - right)) value = signed/scale (signed/positive left) value - signed/scale (signed/negative left) value - (signed/scale (signed/positive right) value - signed/scale (signed/negative right) value)

signed/scale-difference-subtract-value :
  (factor left right : ℚ)
  → signed/scale (signed/positive factor) (left - right) - signed/scale (signed/negative factor) (left - right) = signed/scale (signed/positive factor) left - signed/scale (signed/negative factor) left - (signed/scale (signed/positive factor) right - signed/scale (signed/negative factor) right)

vector/signed-scale-negate-factor :
  (factor : ℚ) (values : List ℚ)
  → vector/equivalent (scale) (vector/negate (vector/signed-scale factor values))
  where scale := vector/signed-scale (signed/negate factor) values

vector/signed-scale-negate-value :
  (factor : ℚ) (values : List ℚ)
  → vector/equivalent (scale) (vector/negate (vector/signed-scale factor values))
  where scale := vector/signed-scale factor (vector/negate values)

vector/signed-scale-subtract-factor :
  (left right : ℚ) (values : List ℚ)
  → vector/equivalent (scale) (subtract)
  where scale := vector/signed-scale (left - right) values
  where subtract := vector/subtract (vector/signed-scale left values) (vector/signed-scale right values)

vector/signed-scale-subtract-value :
  (factor : ℚ) (left right : List ℚ) (same : vector/same-shape left right)
  → vector/equivalent (scale) (subtract)
  where scale := vector/signed-scale factor (vector/subtract left right)
  where subtract := vector/subtract (vector/signed-scale factor left) (vector/signed-scale factor right)

matrix/signed-scale-negate-factor :
  (factor : ℚ) (rows : List (List ℚ))
  → matrix/equivalent (scale) (matrix/negate (matrix/signed-scale factor rows))
  where scale := matrix/signed-scale (signed/negate factor) rows

matrix/signed-scale-negate-value :
  (factor : ℚ) (rows : List (List ℚ))
  → matrix/equivalent (scale) (matrix/negate (matrix/signed-scale factor rows))
  where scale := matrix/signed-scale factor (matrix/negate rows)

matrix/signed-scale-subtract-factor :
  (left right : ℚ) (rows : List (List ℚ))
  → matrix/equivalent (matrix/signed-scale (left - right) rows) (subtract)
  where subtract := matrix/subtract (matrix/signed-scale left rows) (matrix/signed-scale right rows)

matrix/signed-scale-subtract-value :
  (factor : ℚ) (left right : List (List ℚ)) (same : matrix/same-shape left right)
  → matrix/equivalent (scale) (subtract)
  where scale := matrix/signed-scale factor (matrix/subtract left right)
  where subtract := matrix/subtract (matrix/signed-scale factor left) (matrix/signed-scale factor right)