English
For a multipliable f and a subset s, the product over s and the tail product over its complement multiply to the full tprod.
Русский
Для множимого f и подмножества s произведение по s и хвост-произведение по дополнению к s дают полный tprod.
LaTeX
$$$(\prod' x : s, f(x)) \cdot (\prod' x : ↑s^c, f(x)) = \prod' x, f(x).$$$
Lean4
/-- Let `f : β → α` be a multipliable function and let `b ∈ β` be an index.
Lemma `tprod_eq_mul_tprod_ite` writes `∏ n, f n` as `f b` times the product of the
remaining terms. -/
@[to_additive /-- Let `f : β → α` be a summable function and let `b ∈ β` be an index.
Lemma `tsum_eq_add_tsum_ite` writes `Σ' n, f n` as `f b` plus the sum of the
remaining terms. -/
]
protected theorem tprod_eq_mul_tprod_ite [DecidableEq β] (hf : Multipliable f) (b : β) :
∏' n, f n = f b * ∏' n, ite (n = b) 1 (f n) :=
by
rw [(hasProd_ite_div_hasProd hf.hasProd b).tprod_eq]
exact (mul_div_cancel _ _).symm
