prod_mul_prod_eq_prod_zipWith_mul_prod_drop

English

For lists l and l', the products satisfy l.prod · l'.prod = (zipWith (· * ·) l l').prod · (l.drop l'.length).prod · (l'.drop l.length).prod.

Русский

Для списков l и l' произведения удовлетворяют равенству: произведение l умножить на произведение l' равно произведению zipWith на элементы и хвосты.

LaTeX

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

Lean4

@[to_additive]
theorem prod_mul_prod_eq_prod_zipWith_mul_prod_drop :
    ∀ l l' : List M, l.prod * l'.prod = (zipWith (· * ·) l l').prod * (l.drop l'.length).prod * (l'.drop l.length).prod
  | [], ys => by simp
  | xs, [] => by simp
  | x :: xs, y :: ys => by
    simp only [drop, length, zipWith_cons_cons, prod_cons]
    conv =>
      lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
      rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
    simp [mul_assoc]

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