prod_div_prod_filter — Mathlib

English

In a commutative group G, the product of f over g divided by the p-filter product equals the not-p-filter product.

Русский

В коммутативной группе G произведение f по g делится на произведение отфильтрованное по p, равное произведению по не-p.

LaTeX

$$$$ f.\\mathrm{prod} g / (f.filter p).\\mathrm{prod} g = (f.filter (\\lambda a. \\lnot p a)).\\mathrm{prod} g. $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_div_prod_filter [CommGroup G] (g : α → M → G) :
    f.prod g / (f.filter p).prod g = (f.filter fun a => ¬p a).prod g :=
  div_eq_of_eq_mul' (prod_filter_mul_prod_filter_not _ _ _).symm

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