prod_map_div — Mathlib

English

For a multiset m and functions f,g: ι → G in a DivisionCommMonoid G, the product of quotients equals the quotient of products: (m.map (f(i)/g(i))).prod = (m.map f).prod / (m.map g).prod.

Русский

Для мультимножества m и функций f,g:ι → G в DivisionCommMonoid G произведение частных равно частному произведений: (m.map (f(i)/g(i))).prod = (m.map f).prod / (m.map g).prod.

LaTeX

$$$\\big( \\mathrm{prod}( \\mathrm{map}( i \\mapsto f(i)/g(i) )\\, m ) \\big) = \\dfrac{ \\mathrm{prod}( \\mathrm{map} f\, m ) }{ \\mathrm{prod}( \\mathrm{map} g\, m ) }$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_map_div : (m.map fun i => f i / g i).prod = (m.map f).prod / (m.map g).prod :=
  m.prod_hom₂ (· / ·) mul_div_mul_comm (div_one _) _ _

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