English
A two-element reduction of a product where only two elements may be nontrivial; otherwise all are 1.
Русский
Уточнение для произведения: только два элемента могут быть ненулевыми, остальные равны единице.
LaTeX
$$$\text{If } a,b \in s,\; \text{and } f c=1 \text{ for all } c\in s\setminus\{a,b\}, \; \prod_{x\in s} f x = f a \cdot f b$$$
Lean4
@[to_additive]
theorem prod_eq_mul {s : Finset ι} {f : ι → M} (a b : ι) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1)
(ha : a ∉ s → f a = 1) (hb : b ∉ s → f b = 1) : ∏ x ∈ s, f x = f a * f b :=
by
haveI := Classical.decEq ι; by_cases h₁ : a ∈ s <;> by_cases h₂ : b ∈ s
· exact prod_eq_mul_of_mem a b h₁ h₂ hn h₀
· rw [hb h₂, mul_one]
apply prod_eq_single_of_mem a h₁
exact fun c hc hca => h₀ c hc ⟨hca, ne_of_mem_of_not_mem hc h₂⟩
· rw [ha h₁, one_mul]
apply prod_eq_single_of_mem b h₂
exact fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩
· rw [ha h₁, hb h₂, mul_one]
exact
_root_.trans (prod_congr rfl fun c hc => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, ne_of_mem_of_not_mem hc h₂⟩)
prod_const_one
