English
Let e: ι ≃ κ be a bijection. For any f: ι → M and g: κ → M with f x = g (e x) for all x, the products over all elements are equal: ∏ x f(x) = ∏ x g(x).
Русский
Пусть e: ι ≃ κ — биекция. Для любых f: ι → M и g: κ → M с условием f(x) = g(e(x)), произведения по всем элементам равны: ∏ f(x) = ∏ g(x).
LaTeX
$$$$\forall x,\; f(x) = g(e(x)) \Rightarrow \prod_{x} f(x) = \prod_{x} g(x).$$$$
Lean4
/-- `Fintype.prod_equiv` is a specialization of `Finset.prod_bij` that
automatically fills in most arguments.
See `Equiv.prod_comp` for a version without `h`.
-/
@[to_additive /-- `Fintype.sum_equiv` is a specialization of `Finset.sum_bij` that
automatically fills in most arguments.
See `Equiv.sum_comp` for a version without `h`. -/
]
theorem prod_equiv (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ x, f x = g (e x)) : ∏ x, f x = ∏ x, g x :=
prod_bijective _ e.bijective _ _ h
