prod_eq_mul_prod_subtype_ne — Mathlib

English

For f: α → M and a ∈ α, the product over all i equals f(a) times the product over i ≠ a of f(i).

Русский

Для f: α → M и a ∈ α имеем: произведение по всем i равно f(a) умножить на произведение по i ≠ a.

LaTeX

$$$\\prod_{i \\in \\mathrm{univ}} f(i) = f(a) \\cdot \\prod_{i \\in \\mathrm{univ}, i \\neq a} f(i)$$$

Lean4

@[to_additive]
theorem prod_eq_mul_prod_subtype_ne [DecidableEq α] (f : α → M) (a : α) :
    ∏ i, f i = f a * ∏ i : { i // i ≠ a }, f i.1 := by
  simp_rw [← (Equiv.optionSubtypeNe a).prod_comp, prod_option, Equiv.optionSubtypeNe_none, Equiv.optionSubtypeNe_some]

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