finprod_inv_distrib — Mathlib

English

In a division monoid G, the finprod of inverses equals the inverse of the finprod: ∏ᶠ x, (f(x))⁻¹ = (∏ᶠ x, f(x))⁻¹.

Русский

В дивизионном моноиде G произведение в безопасном смысле сохраняет обратное: ∏ᶠ x, (f(x))⁻¹ = (∏ᶠ x, f(x))⁻¹.

LaTeX

$$$$ \prod^{\mathrm{fin}}_{x} (f(x))^{-1} = \left( \prod^{\mathrm{fin}}_{x} f(x) \right)^{-1}. $$$$

Lean4

@[to_additive]
theorem finprod_inv_distrib [DivisionCommMonoid G] (f : α → G) : (∏ᶠ x, (f x)⁻¹) = (∏ᶠ x, f x)⁻¹ :=
  ((MulEquiv.inv G).map_finprod f).symm

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