English
Assume a ∈ l and a list l satisfies that every pair of elements commutes (x y = y x for all x, y in l). Then a · (l.erase a).prod = l.prod.
Русский
Пусть a ∈ l и для любого x, y ∈ l выполняется x y = y x. Тогда a умноженное на произведение l.erase a равно произведению l.
LaTeX
$$$ a \in l \quad \&\quad \forall x \in l, \forall y \in l, x y = y x \Rightarrow a * (l.erase a).prod = l.prod $$$
Lean4
@[to_additive]
theorem prod_erase_of_comm [DecidableEq M] (ha : a ∈ l) (comm : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x) :
a * (l.erase a).prod = l.prod := by
induction l with
| nil => simp only [not_mem_nil] at ha
| cons b l ih =>
obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
· simp only [erase_cons_head, prod_cons]
rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc, comm a ha b mem_cons_self,
mul_assoc, ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
