prod_map_inv' — Mathlib

English

For a multiset m of elements of a DivisionComMonoid G, the product of inverses equals the inverse of the product: (m.map inv).prod = m.prod^{-1}.

Русский

Для мультимножества m элементов DivisionComMonoid G произведение обратных равно обратному произведению: (m.map inv).prod = m.prod^{-1}.

LaTeX

$$$\\big( \\mathrm{prod}( m \\mapsto m^{-1} ) \\big) = \\big( \\mathrm{prod} \\; m \\big)^{-1}$$$

Lean4

@[to_additive]
theorem prod_map_inv' (m : Multiset G) : (m.map Inv.inv).prod = m.prod⁻¹ :=
  m.prod_hom (invMonoidHom : G →* G)

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