English
A variant of List.prod that evaluates to the product in a way that the single-element list {[x]} multiplies to x; this ensures definitional equality for lift/eval operations.
Русский
Вариант List.prod, в котором единичный элемент списка {[x]} даёт произведение x; это обеспечивает дефиниционное равенство для операций подъёма/оценки.
LaTeX
$$$\\\\forall M [Monoid M], \\\\; List\\\\prodAux = \\\\text{fold} \\\\;(* ) \\\\;$$$
Lean4
/-- A variant of `List.prod` that has `[x].prod = x` true definitionally.
The purpose is to make `FreeMonoid.lift_eval_of` true by `rfl`. -/
@[to_additive /-- A variant of `List.sum` that has `[x].sum = x` true definitionally.
The purpose is to make `FreeAddMonoid.lift_eval_of` true by `rfl`. -/
]
def prodAux {M} [Monoid M] : List M → M
| [] => 1
| (x :: xs) => List.foldl (· * ·) x xs
