theorem List.instAssociativeHAdd_hexBasic {R : Type u} [Lean.Grind.Semiring R] : Std.Associative fun (x1 x2 : R) => x1 + x2

Addition in a Grind.Semiring is an associative operation.

theorem List.instAssociativeHMul_hexBasic {R : Type u} [Lean.Grind.Semiring R] : Std.Associative fun (x1 x2 : R) => x1 * x2

Multiplication in a Grind.Semiring is an associative operation.

theorem List.instLawfulIdentityHAddOfNat_hexBasic {R : Type u} [Lean.Grind.Semiring R] : Std.LawfulIdentity (fun (x1 x2 : R) => x1 + x2) 0

0 is a two-sided identity for addition in a Grind.Semiring.

theorem List.instLawfulIdentityHMulOfNat_hexBasic {R : Type u} [Lean.Grind.Semiring R] : Std.LawfulIdentity (fun (x1 x2 : R) => x1 * x2) 1

1 is a two-sided identity for multiplication in a Grind.Semiring.

theorem List.foldl_congr {α : Type v} {β : Type w} (xs : List α) (f g : β → α → β) (z : β) (h : ∀ (acc : β) (x : α), x ∈ xs → f acc x = g acc x) : foldl f z xs = foldl g z xs

Two folds over xs agree when their step functions agree pointwise on the elements of xs (for every accumulator). The fully general fold congruence.

theorem List.foldl_add_congr {α : Type v} {R : Type u} [Add R] (xs : List α) (f g : α → R) (z : R) (h : ∀ (x : α), x ∈ xs → f x = g x) : foldl (fun (acc : R) (x : α) => acc + f x) z xs = foldl (fun (acc : R) (x : α) => acc + g x) z xs

Congruence for an additive fold-sum under its summand f.

theorem List.foldl_mul_congr {α : Type v} {R : Type u} [Mul R] (xs : List α) (f g : α → R) (z : R) (h : ∀ (x : α), x ∈ xs → f x = g x) : foldl (fun (acc : R) (x : α) => acc * f x) z xs = foldl (fun (acc : R) (x : α) => acc * g x) z xs

Congruence for a multiplicative fold-product under its factor f.

theorem List.foldl_mul_eq_mul_foldl {α : Type v} {M : Type u} [Mul M] [One M] [Std.Associative fun (x1 x2 : M) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : M) => x1 * x2) 1] (xs : List α) (f : α → M) (z : M) : foldl (fun (acc : M) (x : α) => acc * f x) z xs = z * foldl (fun (acc : M) (x : α) => acc * f x) 1 xs

Pull the running accumulator out of a multiplicative fold-product, taking the product from a 1 start. Stated for any associative multiplication with a two-sided unit, so it applies to monoids that are not Grind rings (e.g. the executable polynomial types).

theorem List.foldl_const_step {α : Type v} {β : Type w} (xs : List α) (z : β) : foldl (fun (acc : β) (x : α) => acc) z xs = z

Folding with a step that discards the element and returns the accumulator unchanged yields the initial accumulator. (Core's List.foldl_const is the unrelated iterate lemma, hence the name.)

theorem List.foldl_add_perm {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (f : α → R) {xs ys : List α} (h : xs.Perm ys) (z : R) : foldl (fun (acc : R) (x : α) => acc + f x) z xs = foldl (fun (acc : R) (x : α) => acc + f x) z ys

An additive fold-sum is invariant under permuting the list.

theorem List.foldl_mul_perm {α : Type v} {R : Type u} [Lean.Grind.CommSemiring R] (f : α → R) {xs ys : List α} (h : xs.Perm ys) (z : R) : foldl (fun (acc : R) (x : α) => acc * f x) z xs = foldl (fun (acc : R) (x : α) => acc * f x) z ys

A multiplicative fold-product is invariant under permuting the list.

theorem List.foldl_add_eq_add_foldl {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (f : α → R) (z : R) : foldl (fun (acc : R) (x : α) => acc + f x) z xs = z + foldl (fun (acc : R) (x : α) => acc + f x) 0 xs

Pull the running accumulator out of an additive fold-sum, taking the sum from a 0 start. The additive twin of foldl_mul_eq_mul_foldl.

theorem List.foldl_add_eq_self {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (f : α → R) (z : R) (h : ∀ (x : α), x ∈ xs → f x = 0) : foldl (fun (acc : R) (x : α) => acc + f x) z xs = z

An additive fold-sum whose every summand vanishes on xs returns the initial accumulator.

theorem List.foldl_add_zero {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (z : R) : foldl (fun (acc : R) (x : α) => acc + 0) z xs = z

An additive fold-sum whose body adds a literal 0 returns the initial accumulator.

theorem List.foldl_add_mul_left {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (c : R) (f : α → R) (z : R) : foldl (fun (acc : R) (x : α) => acc + c * f x) (c * z) xs = c * foldl (fun (acc : R) (x : α) => acc + f x) z xs

Factor a left scalar out of an additive fold-sum.

theorem List.foldl_add_mul_left_zero {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (c : R) (f : α → R) : foldl (fun (acc : R) (x : α) => acc + c * f x) 0 xs = c * foldl (fun (acc : R) (x : α) => acc + f x) 0 xs

Factor a left scalar out of an additive fold-sum started from 0.

theorem List.foldl_add_mul_right {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (f : α → R) (c z : R) : foldl (fun (acc : R) (x : α) => acc + f x) z xs * c = foldl (fun (acc : R) (x : α) => acc + f x * c) (z * c) xs

Factor a right scalar out of an additive fold-sum (right distributivity, no commutativity needed).

theorem List.foldl_add_neg {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f : α → R) (z : R) : foldl (fun (acc : R) (x : α) => acc + -f x) (-z) xs = -foldl (fun (acc : R) (x : α) => acc + f x) z xs

Negation distributes through an additive fold-sum.

theorem List.foldl_add_add_start {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (f g : α → R) (a b : R) : foldl (fun (acc : R) (x : α) => acc + (f x + g x)) (a + b) xs = foldl (fun (acc : R) (x : α) => acc + f x) a xs + foldl (fun (acc : R) (x : α) => acc + g x) b xs

An additive fold-sum of a pointwise sum splits into two folds, distributing the starting accumulator.

theorem List.foldl_add_add_of_acc {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (f g : α → R) (acc accF accG : R) (h : acc = accF + accG) : foldl (fun (acc : R) (x : α) => acc + (f x + g x)) acc xs = foldl (fun (acc : R) (x : α) => acc + f x) accF xs + foldl (fun (acc : R) (x : α) => acc + g x) accG xs

An additive fold-sum of a pointwise sum splits into two folds, given a splitting of the starting accumulator.

theorem List.foldl_add_add {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (f g : α → R) : foldl (fun (acc : R) (x : α) => acc + (f x + g x)) 0 xs = foldl (fun (acc : R) (x : α) => acc + f x) 0 xs + foldl (fun (acc : R) (x : α) => acc + g x) 0 xs

An additive fold-sum of a pointwise sum from 0 splits into the sum of the two separate folds from 0.

theorem List.foldl_add_sub {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f g : α → R) (a b : R) : foldl (fun (acc : R) (x : α) => acc + (f x - g x)) (a - b) xs = foldl (fun (acc : R) (x : α) => acc + f x) a xs - foldl (fun (acc : R) (x : α) => acc + g x) b xs

An additive fold-sum of a pointwise difference splits into the difference of the two fold-sums, distributing the starting accumulator.

theorem List.foldl_add_sub_zero {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f g : α → R) : foldl (fun (acc : R) (x : α) => acc + (f x - g x)) 0 xs = foldl (fun (acc : R) (x : α) => acc + f x) 0 xs - foldl (fun (acc : R) (x : α) => acc + g x) 0 xs

An additive fold-sum of a pointwise difference from 0 splits into the difference of the two fold-sums from 0.

theorem List.foldl_add_comm {α : Type v} {R : Type u} [Lean.Grind.Semiring R] {γ : Type w} (xs : List α) (ys : List γ) (f : α → γ → R) : foldl (fun (acc : R) (x : α) => acc + foldl (fun (acc' : R) (y : γ) => acc' + f x y) 0 ys) 0 xs = foldl (fun (acc : R) (y : γ) => acc + foldl (fun (acc' : R) (x : α) => acc' + f x y) 0 xs) 0 ys

Sum-swap (Fubini) for nested additive fold-sums.

theorem List.foldl_add_mul_right_zero {α : Type v} {R : Type u} [Lean.Grind.Semiring R] (xs : List α) (f : α → R) (c : R) : foldl (fun (acc : R) (x : α) => acc + f x * c) 0 xs = foldl (fun (acc : R) (x : α) => acc + f x) 0 xs * c

Factor a right scalar out of an additive fold-sum started from 0.

theorem List.foldl_add_flatMap {α : Type v} {R : Type u} [Add R] {γ : Type w} (xs : List α) (f : α → List γ) (g : γ → R) (z : R) : foldl (fun (acc : R) (x : γ) => acc + g x) z (flatMap f xs) = foldl (fun (acc : R) (x : α) => foldl (fun (acc : R) (y : γ) => acc + g y) acc (f x)) z xs

An additive fold-sum over xs.flatMap f equals the fold over xs whose body folds each sublist f x into the accumulator.

theorem List.foldl_add_single {α : Type v} {R : Type u} [Lean.Grind.Semiring R] [DecidableEq α] (xs : List α) (z : R) (q : α) (f : α → R) (hmem : q ∈ xs) (hnodup : xs.Nodup) : foldl (fun (acc : R) (x : α) => acc + if x = q then f x else 0) z xs = z + f q

An additive fold-sum over a Nodup list whose summand is supported at a single matching element collects exactly that summand.

theorem List.le_foldl_add_self {α : Type v} (xs : List α) (g : α → Nat) (init : Nat) : init ≤ foldl (fun (acc : Nat) (x : α) => acc + g x) init xs

An additive fold-sum over Nat is at least its starting accumulator.

theorem List.le_foldl_add_of_mem {α : Type v} (xs : List α) (g : α → Nat) {x : α} {init : Nat} (hx : x ∈ xs) : g x ≤ foldl (fun (acc : Nat) (y : α) => acc + g y) init xs

Every summand is bounded by an additive fold-sum over Nat that contains it.

theorem List.le_foldl_max_self {α : Type v} (xs : List α) (g : α → Nat) (init : Nat) : init ≤ foldl (fun (acc : Nat) (x : α) => max acc (g x)) init xs

A Nat fold-max is at least its starting accumulator.

theorem List.le_foldl_max_of_mem {α : Type v} (xs : List α) (g : α → Nat) {x : α} {init : Nat} (hx : x ∈ xs) : g x ≤ foldl (fun (acc : Nat) (y : α) => max acc (g y)) init xs

Every element's value is bounded by a Nat fold-max that contains it.