Theorems · Theorem · order theory

Finset.prod_Iio_add_one

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

Defined in

Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidLinearOrderLocallyFiniteOrderBotAddOneSuccAddOrderNoMaxOrder