English
The snd-coordinate of the product over a list equals the sum over indices of products of the fst components before and after the index, multiplied by the corresponding snd component.
Русский
Вторая координата произведения списка равна сумме по индексам произведений перед и после индекса первых координат, помноженных на соответствующую вторую координату.
LaTeX
$$$\\\\mathrm{snd}(\\\\mathrm{List}.prod l) = \\.sum_{i} (\\\\prod_{ji} l_j.fst)$$$
Lean4
/-- The second element of a product $\prod_{i=0}^n (r_i + m_i)$ is a sum of terms of the form
$r_0\cdots r_{i-1}m_ir_{i+1}\cdots r_n$. -/
theorem snd_list_prod [Monoid R] [AddCommMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M)) :
l.prod.snd =
(l.zipIdx.map fun x : tsze R M × ℕ =>
((l.map fst).take x.2).prod •> x.fst.snd <• ((l.map fst).drop x.2.succ).prod).sum :=
by
induction l with
| nil => simp
| cons x xs ih =>
rw [List.zipIdx_cons']
simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id, List.take_zero,
List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul, List.drop, mul_smul, List.sum_cons,
fst_list_prod, ih, List.smul_sum, List.map_map, ← smul_comm (_ : R) (_ : Rᵐᵒᵖ)]
exact add_comm _ _
