prod_eq_mul_prod_compl — Mathlib

English

For any a in the index type, ∏ i f(i) equals f(a) times the product over all i not equal to a: ∏ i, f(i) = f(a) · ∏ i∈{a}^c, f(i).

Русский

Для любого элемента a из типа индексов верно: ∏_{i} f(i) = f(a) · ∏_{i ∈ {a}^c} f(i).

LaTeX

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

Lean4

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

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