hasProd_iff_compl — Mathlib

English

For a Finset s, HasProd f a is equivalent to HasProd (f x) on the complement with a divisor relation using s’s product.

Русский

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

LaTeX

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

Lean4

@[to_additive]
protected theorem hasProd_iff_compl (s : Finset β) :
    HasProd f a ↔ HasProd (fun x : { x // x ∉ s } ↦ f x) (a / ∏ i ∈ s, f i) :=
  (s.hasProd f).hasProd_iff_compl

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