prod_eq_prod_compl_mul — Mathlib

English

For any a ∈ ι and f: ι → M, ∏ i f(i) equals (∏ i ∈ {a}^c, f(i)) · f(a).

Русский

Для любого a ∈ ι и функции f: ∏_{i} f(i) = (∏_{i ∈ {a}^c} f(i)) · f(a).

LaTeX

$$$\\displaystyle \\prod_{i} f(i) = \\left(\\prod_{i \\in {a}^{c}} f(i)\\right) \\cdot f(a)$$$

Lean4

@[to_additive]
theorem _root_.Fintype.prod_eq_prod_compl_mul [DecidableEq ι] [Fintype ι] (a : ι) (f : ι → M) :
    ∏ i, f i = (∏ i ∈ { a }ᶜ, f i) * f a :=
  prod_eq_prod_diff_singleton_mul (mem_univ a) f

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