Reference · Signed rationals

rainbow.math.rational.signed.distributive

Signed rationalssrc/rainbow/math/rational/signed/distributive.clj0 definitions, 3 theorems

Distributivity of signed multiplication over addition, and the scaled finite sum. signed/multiply-zero-left 0*a ~ 0 signed/multiply-distributes-add-right (a+b)*m ~ a*m + b*m signed/map-sum-scale-right (sum f) * c ~ sum (f * c) Unfolded, the distributive law is an eight-monomial identity in six component atoms; the zero law is a three-monomial one with `nnrat/zero` as a further opaque atom. Both are pure semiring identities, so each is a single `rainbow.math.rational.nnrat.ring` call. `signed/map-sum-scale-right` is the one proof with induction in it: the empty sum scales by the zero law and the cons step is distributivity against the induction hypothesis. It is the pull-a-scalar-through-a-sum step of every dot-product rearrangement. Native and axiom-free; chains the signed multiplicative ring laws and the nnrat-ring tactic on D63.

Depends onmath.rational.signed.multiply-ring

signed/multiply-zero-left :
  (a : ℚ)
  → 0 · a = 0

signed/multiply-distributes-add-right :
  (a b m : ℚ)
  → (a + b) · m = a · m + b · m

signed/map-sum-scale-right.{u} :
  (A : Type u) (f : A → ℚ) (c : ℚ) (xs : List A)
  → (Σ j∈xs, f j) · c = Σ i∈xs, f i · c