prod_Ioi_zero

Mathlib.Algebra.BigOperators.Fin

URI: https://scilib.ai/kg/mathlib#Fin.prod_Ioi_zero

English

Let f: Fin(n+1) → M. Then the product over i > 0 equals the product over j: Fin n of f(j.succ).

Русский

Пусть f: Fin(n+1) → M. Тогда произведение по i > 0 равно произведению по j: Fin n от f(j.succ).

LaTeX

$$$$\\prod_{i>0} f(i) = \\prod_{j: Fin n} f(j.succ).$$$$

Lean4

@[to_additive]
theorem prod_Ioi_zero (f : Fin (n + 1) → M) : ∏ i > 0, f i = ∏ j : Fin n, f j.succ := by simp [Ioi_zero_eq_map]

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

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

Разделы

Аффилиация

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