finprod_comp — Mathlib

English

If e: α → β is a bijection and g: β → M, then ∏ᶠ i, g(e(i)) = ∏ᶠ j, g(j).

Русский

Если e: α → β биекция и g: β → M, то ∏ᶠ i, g(e(i)) = ∏ᶠ j, g(j).

LaTeX

$$$\\prod^\\!f i, g(e(i)) = \\prod^\\!f j, g(j)$$$

Lean4

/-- See also `finprod_eq_of_bijective`, `Fintype.prod_bijective` and `Finset.prod_bij`. -/
@[to_additive /-- See also `finsum_eq_of_bijective`, `Fintype.sum_bijective` and `Finset.sum_bij`. -/
    ]
theorem finprod_comp {g : β → M} (e : α → β) (he₀ : Function.Bijective e) : (∏ᶠ i, g (e i)) = ∏ᶠ j, g j :=
  finprod_eq_of_bijective e he₀ fun _ => rfl

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