English
For a commutative monoid, the product of the elements of x and y equals the product of the zipWith product: x.toList.prod * y.toList.prod = (Vector.zipWith (· * ·) x y).toList.prod.
Русский
Для коммутативного моноида произведение элементов x и y равно произведению элементов, полученных через zipWith: x.toList.prod * y.toList.prod = (Vector.zipWith (· * ·) x y).toList.prod.
LaTeX
$$$\text{CommMonoid } α \Rightarrow x.toList.prod * y.toList.prod = (Vector.zipWith (\cdot * \cdot) x y).toList.prod$$$
Lean4
@[to_additive]
theorem prod_mul_prod_eq_prod_zipWith [CommMonoid α] (x y : Vector α n) :
x.toList.prod * y.toList.prod = (Vector.zipWith (· * ·) x y).toList.prod :=
List.prod_mul_prod_eq_prod_zipWith_of_length_eq x.toList y.toList ((toList_length x).trans (toList_length y).symm)
