English
The product (over a finite set s) of singles equals a single with the product of the indices and the product of the scalars: ∏ i∈s single (m i) (r i) = single (∏ i∈s m i) (∏ i∈s r i).
Русский
Произведение по конечному множеству s элементарных единичных элементов равно единичному элементу, соответствующему произведению индексов и произведению скаляров.
LaTeX
$$$\\prod i\\in s\\; \\mathrm{single}(m(i), r(i)) = \\mathrm{single}\\Big(\\prod i\\in s\\; m(i)\\Big)\\Big(\\prod i\\in s\\; r(i)\\Big).$$$
Lean4
@[to_additive (dont_translate := R) prod_single]
theorem prod_single (s : Finset ι) (m : ι → M) (r : ι → R) :
∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i) :=
Finset.cons_induction_on s rfl fun i s hi ih ↦ by rw [prod_cons, ih, single_mul_single, prod_cons, prod_cons]
