Theorems · Theorem · combinatorics

Fintype.prod_eq_mul

∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : CommMonoid M] {f : α → M} (a b : α),
  a ≠ b → (∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1) → ∏ x, f x = f a * f b

Defined in

Mathlib.Data.Fintype.BigOperators

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeCommMonoid