English
If two lists l1 and l2 are permutations of each other, and the elements of l1 pairwise commute, then their products are equal: l1.prod = l2.prod.
Русский
Если два списка l1 и l2 являются перестановками друг друга, и элементы l1 взаимно коммутируют попарно, то их произведения равны: l1.prod = l2.prod.
LaTeX
$$l1.Perm l2 → l1.Pairwise Commute → l1.prod = l2.prod$$
Lean4
/-- If elements of a list commute with each other, then their product does not
depend on the order of elements. -/
@[to_additive /-- If elements of a list additively commute with each other, then their sum does not
depend on the order of elements. -/
]
theorem prod_eq' (h : l₁ ~ l₂) (hc : l₁.Pairwise Commute) : l₁.prod = l₂.prod :=
by
refine h.foldr_eq' ?_ _
apply Pairwise.forall_of_forall
· intro x y h z
exact (h z).symm
· intros; rfl
· apply hc.imp
intro a b h z
rw [← mul_assoc, ← mul_assoc, h]
