Reference · Matrices

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

Matricessrc/rainbow/math/linear/matrix/signed_scale_units.clj0 definitions, 9 theorems

Scalar-factor additivity and zero/one laws for signed matrix scaling. The scale-difference representation distributes over addition in its signed factor, sends zero to shaped zero, and sends one to the original value. Structural lifts complete these module laws for vectors and matrices without shape premises. Native and axiom-free on D63.

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

signed/scale-difference-additive-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-zero :
  (value : ℚ)
  → signed/scale (signed/positive 0) value - signed/scale (signed/negative 0) value = 0

signed/scale-difference-one :
  (value : ℚ)
  → signed/scale (signed/positive 1) value - signed/scale (signed/negative 1) value = value

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

vector/signed-scale-zero :
  (values : List ℚ)
  → vector/equivalent (vector/signed-scale 0 values) (vector/zero-like values)

vector/signed-scale-one :
  (values : List ℚ)
  → vector/equivalent (vector/signed-scale 1 values) values

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

matrix/signed-scale-zero :
  (rows : List (List ℚ))
  → matrix/equivalent (matrix/signed-scale 0 rows) (matrix/zero-like rows)

matrix/signed-scale-one :
  (rows : List (List ℚ))
  → matrix/equivalent (matrix/signed-scale 1 rows) rows