finprod_comp_equiv

Mathlib.Algebra.BigOperators.Finprod

URI: https://scilib.ai/kg/mathlib#finprod_comp_equiv

English

Let e: α ≃ β be a bijection. For any f: β → M, ∏ᶠ i, f(e(i)) = ∏ᶠ i, f(i).

Русский

Пусть e: α ≃ β — биекция. При любом f: β → M имеем ∏ᶠ i, f(e(i)) = ∏ᶠ i, f(i).

LaTeX

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

Lean4

@[to_additive]
theorem finprod_comp_equiv (e : α ≃ β) {f : β → M} : (∏ᶠ i, f (e i)) = ∏ᶠ i', f i' :=
  finprod_comp e e.bijective

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

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

Разделы

Аффилиация

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