prod_pair — Mathlib

English

If a and b are distinct, the product over the two-element set {a,b} equals f(a) f(b).

Русский

Если a и b различны, произведение по множеству {a,b} равно f(a) f(b).

LaTeX

$$$a \\neq b \\Rightarrow \\prod_{x \\in \\{a,b\\}} f(x) = f(a)f(b)$$$

Lean4

@[to_additive]
theorem prod_pair [DecidableEq ι] {a b : ι} (h : a ≠ b) : (∏ x ∈ ({ a, b } : Finset ι), f x) = f a * f b := by
  rw [prod_insert (notMem_singleton.2 h), prod_singleton]

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