ite_one_prod — Mathlib

English

Reiterates that the product over a Finset with an if-then-else inside the factors reduces to the corresponding if-then-else of the products.

Русский

Повторяет, что произведение с условной частью внутри множителей сводится к соответствующему условному произведению.

LaTeX

$$$\\prod x \\in s, \\; \\mathrm{ite}\\; p \\; (f x) \\; (g x) = \\mathrm{ite}\\; p \\; (\\prod x \\in s, f x) \\; (\\prod x \\in s, g x)$$$

Lean4

@[to_additive]
theorem ite_one_prod (p : Prop) [Decidable p] (s : Finset ι) (f : ι → M) :
    (if p then 1 else (∏ x ∈ s, f x)) = ∏ x ∈ s, if p then 1 else f x := by simp only [prod_ite_irrel, prod_const_one]

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