Theorems · Theorem · order theory

Finset.sum_Iic_add_zero_comm

∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : Add α] [inst_4 : One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M),
  ∑ i ≤ a + 1, f i = f (a + 1) + ∑ i ≤ a, f i

Defined in

Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Cited by

1 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidLinearOrderLocallyFiniteOrderBotAddOneSuccAddOrderNoMaxOrder