Products of lists of pairwise products with central second factors

List.prod_map_mul splits the product of a list of pairwise products f i * g i into the product of the f i times the product of the g i, in a commutative monoid. The same splitting holds in any monoid as soon as the second factors are central, since each g i can then be moved past the remaining first factors.

Main results

• List.prod_map_mul_of_mem_center: ∏ (f i * g i) = (∏ f i) * (∏ g i) along a list, when g i lies in the center for every entry i of the list.

theorem List.prod_map_mul_of_mem_center {ι : Type u_1} {M : Type u_2} [Monoid M] (l : List ι) (f g : ι → M) (hg : ∀ i ∈ l, g i ∈ Submonoid.center M) : (map (fun (i : ι) => f i * g i) l).prod = (map f l).prod * (map g l).prod

Splitting a product of pairwise products with central second factors. Along a list, the product of the f i * g i is the product of the f i times the product of the g i, provided g i is central for every entry i of the list.