finprod_mem_inv_distrib — Mathlib

English

In a DivisionComMonoid G, for any finite index set s and function f: α → G, the product of inverses equals the inverse of the product: ∏_{x∈s} f(x)^{-1} = (∏_{x∈s} f(x))^{-1}.

Русский

В DivisionComMonoid G для любого конечного индекса s и функции f: α → G произведение обратных элементов равно обратному произведению: ∏_{x∈s} f(x)^{-1} = (∏_{x∈s} f(x))^{-1}.

LaTeX

$$\operatorname{Finite}(s) \Rightarrow \left(\prod_{i \in s} f(i)\right)^{-1} = \prod_{i \in s} f(i)^{-1}$$

Lean4

@[to_additive]
theorem finprod_mem_inv_distrib [DivisionCommMonoid G] (f : α → G) (hs : s.Finite) :
    (∏ᶠ x ∈ s, (f x)⁻¹) = (∏ᶠ x ∈ s, f x)⁻¹ :=
  ((MulEquiv.inv G).map_finprod_mem f hs).symm

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