prod_reverse

Mathlib.Algebra.BigOperators.Group.List.Basic

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

English

The product of a list is unchanged by reversing the list: prod(l.reverse) = prod(l).

Русский

Произведение списка не изменяется при его развороте: prod(l.reverse) = prod(l).

LaTeX

$$$ \mathrm{prod}(l.reverse) = \mathrm{prod}(l) $$$

Lean4

@[to_additive (attr := simp)]
theorem prod_reverse (l : List M) : prod l.reverse = prod l :=
  (reverse_perm l).prod_eq

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

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

Разделы

Аффилиация

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