prod_comp

Mathlib.Algebra.BigOperators.Group.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.prod_comp

English

Let e: ι ≃ κ be a finite equivalence and g: κ → M. Then ∏ i g(e(i)) = ∏ i g(i).

Русский

Пусть e: ι ≃ κ — конечное эквивалентное отображение. Тогда ∏ i g(e(i)) = ∏ i g(i).

LaTeX

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

Lean4

@[to_additive]
theorem _root_.Equiv.prod_comp (e : ι ≃ κ) (g : κ → M) : ∏ i, g (e i) = ∏ i, g i :=
  prod_equiv e _ _ fun _ ↦ rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru