prod_inv_distrib — Mathlib

English

In a division-commutative monoid G, the product of inverses equals the inverse of the product: ∏_{x∈s} f(x)^{-1} = (∏_{x∈s} f(x))^{-1}.

Русский

В делимо-перемещаемом мономоде G произведение обратных равно обратному произведению: ∏ f(x)^{-1} = (∏ f(x))^{-1}.

LaTeX

$$$$\prod_{x \in s} f(x)^{-1} = \left(\prod_{x \in s} f(x)\right)^{-1}.$$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_inv_distrib (f : ι → G) : (∏ x ∈ s, (f x)⁻¹) = (∏ x ∈ s, f x)⁻¹ :=
  Multiset.prod_map_inv

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