prod_comp — Mathlib

English

For a bijection e: ι → κ and a function g: κ → M, the products ∏_{i} g(e(i)) and ∏_{i} g(i) are equal.

Русский

Для биекции e: ι → κ и функции g: κ → M произведения ∏_{i} g(e(i)) и ∏_{i} g(i) равны.

LaTeX

$$$$\prod_{i} g(e(i)) = \prod_{i} g(i).$$$$

Lean4

@[to_additive]
theorem _root_.Function.Bijective.prod_comp {e : ι → κ} (he : e.Bijective) (g : κ → M) : ∏ i, g (e i) = ∏ i, g i :=
  prod_bijective _ he _ _ fun _ ↦ rfl

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