prod_mul_prod_eq_prod_zipWith_of_length_eq

English

If l and l' have the same length, then l.prod · l'.prod = (zipWith (· * ·) l l').prod.

Русский

Если длины списков l и l' равны, то произведение l и произведение l' равно произведению zipWith на эти списки.

LaTeX

$$$ l.length = l'.length \Rightarrow l.prod * l'.prod = (zipWith (\cdot \cdot) l l').prod $$$

Lean4

@[to_additive]
theorem prod_mul_prod_eq_prod_zipWith_of_length_eq (l l' : List M) (h : l.length = l'.length) :
    l.prod * l'.prod = (zipWith (· * ·) l l').prod :=
  by
  apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop l l').trans
  rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]

Похожие утверждения