prod_take_mul_prod_drop — Mathlib

English

Let L be a finite list in a monoid M and i a natural number. Then the product of the prefix of length i times the product of the suffix starting at i equals the product of the whole list: (L.take i).prod · (L.drop i).prod = L.prod.

Русский

Пусть L — конечный список элементов моноида M и i натуральное число. Тогда произведение префикса длины i и произведение суффикса, начинающегося с i, равны произведению всего списка: (L.take i).prod · (L.drop i).prod = L.prod.

LaTeX

$$$ (L.take i).prod \cdot (L.drop i).prod = L.prod $$$

Lean4

@[to_additive (attr := simp)]
theorem prod_take_mul_prod_drop (L : List M) (i : ℕ) : (L.take i).prod * (L.drop i).prod = L.prod := by
  simp [← prod_append]

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