prod_eq_single — Mathlib

English

If a ∈ s, and all other elements c ∈ s with c ≠ a contribute 1, then the product is f(a).

Русский

Если a ∈ s и все прочие элементы дают 1, то произведение равно f(a).

LaTeX

$$$\text{If } a\in s, \; \prod_{x\in s} f x = f a$$$

Lean4

@[to_additive]
theorem prod_eq_single {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) (h₁ : a ∉ s → f a = 1) :
    ∏ x ∈ s, f x = f a :=
  haveI := Classical.decEq ι
  by_cases (prod_eq_single_of_mem a · h₀) fun this =>
    (prod_congr rfl fun b hb => h₀ b hb <| by rintro rfl; exact this hb).trans <| prod_const_one.trans (h₁ this).symm

Похожие утверждения