Theorems · Theorem · group theory

finsum_induction

∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] {f : α → M} (p : M → Prop),
  p 0 → (∀ (x y : M), p x → p y → p (x + y)) → (∀ (i : α), p (f i)) → p (∑ᶠ (i : α), f i)

To prove a property of a finite sum, it suffices to prove that the property is additive and holds on the summands.

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoid