prod_map_inv — Mathlib

English

For a multiset m and a family f: ι → G in a DivisionComMonoid G, the product of inverses equals the inverse of the product: (m.map (i ↦ f(i))^{-1}).prod = (m.map f).prod^{-1}.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem prod_map_inv : (m.map fun i => (f i)⁻¹).prod = (m.map f).prod⁻¹ := by
  rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]

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