prod_eq_mul — Mathlib

English

If a ≠ b and f(x) = 1 for all x ≠ a, b, then the product over α equals f(a) · f(b).

Русский

Если a ≠ b и f(x)=1 для всех x ≠ a,b, то произведение по α равно f(a) · f(b).

LaTeX

$$$\\prod_{x \\in \\mathrm{univ}} f(x) = f(a) \\cdot f(b)\\quad \\text{given } a \\neq b \\text{ and } f(x)=1\\ (x\\neq a,b)$$$

Lean4

@[to_additive]
theorem prod_eq_mul {f : α → M} (a b : α) (h₁ : a ≠ b) (h₂ : ∀ x, x ≠ a ∧ x ≠ b → f x = 1) : ∏ x, f x = f a * f b := by
  apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx <;> exact fun hc => (hc (Finset.mem_univ _)).elim

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