English
Let e: α → β be a bijection and let f: α → M, g: β → M satisfy f(x) = g(e(x)) for all x. Then the finite products agree: ∏ᶠ i, f(i) = ∏ᶠ j, g(j).
Русский
Пусть e: α → β биекция и функции f: α → M, g: β → M удовлетворяют f(x) = g(e(x)) для всех x. Тогда конечные произведения совпадают: ∏ᶠ i, f(i) = ∏ᶠ j, g(j).
LaTeX
$$$\\prod^\\!f i, f(i) = \\prod^\\!f j, g(j)$$$
Lean4
/-- See `finprod_comp`, `Fintype.prod_bijective` and `Finset.prod_bij`. -/
@[to_additive /-- See `finsum_comp`, `Fintype.sum_bijective` and `Finset.sum_bij`. -/
]
theorem finprod_eq_of_bijective {f : α → M} {g : β → M} (e : α → β) (he₀ : Bijective e) (he₁ : ∀ x, f x = g (e x)) :
∏ᶠ i, f i = ∏ᶠ j, g j := by
rw [← finprod_mem_univ f, ← finprod_mem_univ g]
exact finprod_mem_eq_of_bijOn _ (bijective_iff_bijOn_univ.mp he₀) fun x _ => he₁ x
