prod_coe_sort_eq_attach

Mathlib.Algebra.BigOperators.Group.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.prod_coe_sort_eq_attach

English

The product over a finite set s of a function f on s is equal to the product over its attach s.attach of the same function

Русский

Произведение по s равно произведению по attach s.attach той же функции.

LaTeX

$$$\\prod i : s, f i = \\prod i ∈ s.\\!\\text{attach}, f i$$$

Lean4

@[to_additive]
theorem prod_coe_sort_eq_attach (f : s → M) : ∏ i : s, f i = ∏ i ∈ s.attach, f i :=
  rfl

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

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

Разделы

Аффилиация

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