prod_one_cons

Mathlib.Algebra.BigOperators.Group.List.Defs

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

English

In a monoid M, for any list l, (1 :: l).prod = l.prod; prepending the unit does not change the product.

Русский

В моноиде M для любого списка l произведение (1 :: l) равно произведению l; единица не меняет произведение.

LaTeX

$$$ (1 :: l).prod = l.prod $$$

Lean4

@[to_additive]
theorem prod_one_cons : (1 :: l).prod = l.prod := by rw [prod, foldr, one_mul]

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

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

Разделы

Аффилиация

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