prod_eq

Mathlib.Algebra.BigOperators.Group.List.Basic

URI: https://scilib.ai/kg/mathlib#List.Perm.prod_eq

English

If every x ∈ l commutes with y, then l.prod commutes with y.

Русский

Если каждый элемент списка l коммутирует с y, то произведение списка коммутирует с y.

LaTeX

$$$ (\forall x \in l, Commute x y) \Rightarrow Commute l.prod y $$$

Lean4

@[to_additive]
theorem prod_eq (h : Perm l₁ l₂) : prod l₁ = prod l₂ :=
  h.foldr_op_eq

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

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

Разделы

Аффилиация

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