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