prod_ofFn

Mathlib.Algebra.BigOperators.Fin

URI: https://scilib.ai/kg/mathlib#List.prod_ofFn

English

The product of the list List.ofFn f equals the product over all i of f i.

Русский

Произведение списка List.ofFn f равно произведению по всем i от f i.

LaTeX

$$$\\big(\\mathrm{List.ofFn} f\\big).prod = \\prod_{i} f(i)$$$

Lean4

@[to_additive]
theorem prod_ofFn {n : ℕ} {f : Fin n → M} : (ofFn f).prod = ∏ i, f i :=
  Fin.prod_ofFn f

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

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

Разделы

Аффилиация

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