English
Let ι be a finite index set and M a commutative monoid with identity 1. For any predicate p on ι and any function f: ι → M, the product of f over the p-slice of ι times the product over the complement equals the product over all of ι. In symbols: (∏ i : { x | p x }, f i) · (∏ i : { x | ¬ p x }, f i) = ∏ i, f i.
Русский
Пусть ι — конечное множество индексов, M — коммутативный моноид с единицей 1. Пусть p — предикат на ι, и f: ι → M. Тогда произведение f по элементам, удовлетворяющим p, умноженное на произведение по элементам вне p, равно произведению по всем элементам ι: (∏ i : { x | p x }, f i) · (∏ i : { x | ¬ p x }, f i) = ∏ i, f i.
LaTeX
$$$$(\\prod i : \\{ x \\mid p x \\}, f i) \\cdot (\\prod i : \\{ x \\mid \\neg p x \\}, f i) = \\prod i, f i$$$$
Lean4
@[to_additive]
theorem prod_subtype_mul_prod_subtype (p : ι → Prop) (f : ι → M) [DecidablePred p] :
(∏ i : { x // p x }, f i) * ∏ i : { x // ¬p x }, f i = ∏ i, f i := by
classical
let s := {x | p x}.toFinset
rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
· exact Finset.prod_mul_prod_compl _ _
· simp [s]
· simp [s]
