hasProd_compl_iff — Mathlib

English

For a Finset s, HasProd f a is equivalent to HasProd (f x) on the complement of s with a scaled value a multiplied by the product over s of f i.

Русский

Для Finset s эквивалентно HasProd f a и HasProd на дополнении s с умножением на произведение по s.

LaTeX

$$HasProd f a ↔ HasProd (fun x : { x // x ∉ s } ↦ f x) (a * ∏ i ∈ s, f i)$$

Lean4

@[to_additive]
protected theorem hasProd_compl_iff (s : Finset β) :
    HasProd (fun x : { x // x ∉ s } ↦ f x) a ↔ HasProd f (a * ∏ i ∈ s, f i) :=
  (s.hasProd f).hasProd_compl_iff.trans <| by rw [mul_comm]

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