English
For any list L in a monoid M, the product equals the head element multiplied by the product of the tail: L.headI * L.tail.prod = L.prod (using a default 1 when empty).
Русский
Для любого списка L из моноида M произведение равно头 элемента, умноженному на произведение хвоста: L.headI · L.tail.prod = L.prod (при пустом списке — 1).
LaTeX
$$$ l[0]?.getD 1 \cdot l.tail.prod = l.prod $$$
Lean4
/-- We'd like to state this as `L.headI * L.tail.prod = L.prod`, but because `L.headI` relies on an
inhabited instance to return a garbage value on the empty list, this is not possible.
Instead, we write the statement in terms of `L[0]?.getD 1`.
-/
@[to_additive /-- We'd like to state this as `L.headI + L.tail.sum = L.sum`, but because `L.headI`
relies on an inhabited instance to return a garbage value on the empty list, this is not possible.
Instead, we write the statement in terms of `L[0]?.getD 0`. -/
]
theorem getElem?_zero_mul_tail_prod (l : List M) : l[0]?.getD 1 * l.tail.prod = l.prod := by cases l <;> simp
