Theorems · Theorem · group theory

Finset.prod_eq_mul

∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι),
  a ≠ b → (∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) → (a ∉ s → f a = 1) → (b ∉ s → f b = 1) → ∏ x ∈ s, f x = f a * f b

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoid