English
If e: ι → κ is bijective, then 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)) для всех x, произведения по всем элементам совпадают: ∏ f(x) = ∏ g(x).
LaTeX
$$$$\Big( \forall x,\; f(x) = g(e(x)) \Big) \Rightarrow \prod_{x} f(x) = \prod_{x} g(x).$$$$
Lean4
/-- `Fintype.prod_bijective` is a variant of `Finset.prod_bij` that accepts `Function.Bijective`.
See `Function.Bijective.prod_comp` for a version without `h`. -/
@[to_additive /-- `Fintype.sum_bijective` is a variant of `Finset.sum_bij` that accepts
`Function.Bijective`.
See `Function.Bijective.sum_comp` for a version without `h`. -/
]
theorem prod_bijective (e : ι → κ) (he : e.Bijective) (f : ι → M) (g : κ → M) (h : ∀ x, f x = g (e x)) :
∏ x, f x = ∏ x, g x :=
prod_equiv (.ofBijective e he) (by simp) (by simp [h])
