rainbow.math.sums.value-append

Finite sums src/rainbow/math/sums/value_append.clj0 definitions, 1 theorems

Split the existing expr-sum-value at any Nat offset a: sum F (b+a) ~ sum F a + sum (fn i. F(i+a)) b. All Nat lengths, including zero; no sign or boundedness assumptions. Equality is the existing signed-rational equivalence, not raw-pair Eq.

signed/expr-sum-value-append

TheoremFor all inputsNo axiomsSource

signed/expr-sum-value-append :
  (F : ℕ → ℚ) (a b : ℕ)
  → signed/expr-sum-value F (algebra/nat-add b a) = signed/expr-sum-value F a + signed/expr-sum-value (fun i => F (algebra/nat-add i a)) b

+ = signed/add= = signed/equivalent: equality of rational valuesℕ = data/Natℚ = signed/SignedRational