English
A variant form of the previous statement asserting the same equality for range 1.
Русский
Вариант той же теоремы для диапазона 1.
LaTeX
$$$\displaystyle \prod k \in \mathrm{range}(1), f(k) = f(0)$$$
Lean4
@[to_additive]
theorem prod_list_map_count [DecidableEq ι] (l : List ι) (f : ι → M) :
(l.map f).prod = ∏ m ∈ l.toFinset, f m ^ l.count m := by
induction l with
| nil => simp only [map_nil, prod_nil, count_nil, pow_zero, prod_const_one]
| cons a s IH =>
simp only [List.map, List.prod_cons, toFinset_cons, IH]
by_cases has : a ∈ s.toFinset
· rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _), ←
mul_assoc, count_cons_self, pow_succ']
congr 1
refine prod_congr rfl fun x hx => ?_
rw [count_cons_of_ne (ne_of_mem_erase hx).symm]
rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]
grind [Finset.prod_congr]
