Reference · Finite sums

rainbow.math.sums.of-nat

Finite sumssrc/rainbow/math/sums/of_nat.clj0 definitions, 3 theorems

The bridge between a natural-number count written as the signed literal of-nat n = n/1 (the form the checkers use, e.g. A m = sum p) and a sum of n equal terms: nnrat/of-nat-successor : (k + 1)/1 ~ k/1 + 1 (nnrat equivalence) signed/of-nat-successor : of-nat (k + 1) ~ of-nat k + 1 signed/expr-sum-constant-of-nat : sum_{i<n} c ~ c * of-nat n The nnrat step unfolds to succ (k 1) = (k 1 + 1) 1 in nat, closed by multiply-one-right, add-successor-right and nat-add-zero-right (k 1 does not reduce: multiplication recurses on the left).

Depends onmath.sums.flow-cutmath.nat.semiringmath.nat.strict-below-moremath.rational.signed.geometric-bridgemath.linear.matrix.affine-general-rate-certificatemath.rational.signed.multiply-ringmath.linear.matrix.action-scale

nnrat/of-nat-successor :
  (k : ℕ)
  → nnrat/make (data/succ k) 0 = nnrat/make k 0 + 1

signed/of-nat-successor :
  (k : ℕ)
  → signed/from-nnrat (nnrat/make (data/succ k) 0) = signed/from-nnrat (nnrat/make k 0) + 1

signed/expr-sum-constant-of-nat :
  (c : ℚ) (n : ℕ)
  → signed/expr-sum-value (fun x₂ => c) n = c · signed/from-nnrat (nnrat/make n 0)