English
For a function f : α → M and a ∈ l, the product of the mapped erased list satisfies f(a) times the product of the mapped rest equals the product of mapped original: a ∈ l → f(a) · (l.erase a).map f .prod = (l.map f).prod.
Русский
Для функции f: α → M и элемента a в списке l верно: f(a) произведение отложенной части списка после стирания умноженное на остальные элементы после отображения равняется произведению отображённых элементов всего списка.
LaTeX
$$$ a \in l \Rightarrow f a \cdot ((l.erase a).map f).prod = (l.map f).prod $$$
Lean4
@[to_additive]
theorem prod_map_eq_pow_single [DecidableEq α] {l : List α} (a : α) (f : α → M)
(hf : ∀ a', a' ≠ a → a' ∈ l → f a' = 1) : (l.map f).prod = f a ^ l.count a := by
induction l generalizing a with
| nil => rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
| cons a' as h =>
specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
rw [List.map_cons, List.prod_cons, count_cons, h]
simp only [beq_iff_eq]
split_ifs with ha'
· rw [ha', _root_.pow_succ']
· rw [hf a' ha' mem_cons_self, one_mul, add_zero]
