Theorems · Theorem · combinatorics

Fin.prod_univ_succAbove

∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (x : Fin (n + 1)),
  ∏ i, f i = f x * ∏ i, f (x.succAbove i)

A product of a function f : Fin (n + 1) → M over all Fin (n + 1) is the product of f x, for some x : Fin (n + 1) times the remaining product

Defined in

Mathlib.Algebra.BigOperators.Fin

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommMonoid