prod_eq_single — Mathlib

English

Let f: α → M and a ∈ α with f(x) = 1 for all x ≠ a. Then the product over α equals f(a).

Русский

Пусть f: α → M и a ∈ α так, что f(x)=1 для всех x ≠ a. Тогда произведение по α равно f(a).

LaTeX

$$$\\prod_{x \\in \\mathrm{univ}} f(x) = f(a)\\quad \\text{if } (\\forall x \\in \\mathrm{univ}, x\\neq a \\Rightarrow f(x)=1)$$$

Lean4

@[to_additive]
theorem prod_eq_single {f : α → M} (a : α) (h : ∀ x ≠ a, f x = 1) : ∏ x, f x = f a :=
  Finset.prod_eq_single a (fun x _ hx => h x hx) fun ha => (ha (Finset.mem_univ a)).elim

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