English
Let α be a type with multiplication and one. For every m ≥ 0 and every v: Fin m → α, the product over all indices i of v(i) equals the product ∏_{i : Fin m} v(i). In particular, FinVec.prod a = ∏ i, a i.
Русский
Пусть α — множество с операциями умножения и единицей. Для любого m ≥ 0 и любой функции v: Fin m → α произведение по всем индексам i от v(i) равно ∏_{i ∈ Fin m} v(i). В частности, FinVec.prod a = ∏ i, a i.
LaTeX
$$$\\forall m\\,\\forall a : \\mathrm{Fin}\,m \\to \\alpha,\\quad \\mathrm{FinVec.prod}\\,a = \\prod_{i : \\mathrm{Fin}\,m} a(i).$$$
Lean4
/-- `Finset.univ.prod` with better defeq for `Fin`. -/
@[to_additive existing]
def prod [Mul α] [One α] : ∀ {m} (_ : Fin m → α), α
| 0, _ => 1
| 1, v => v 0
| _ + 2, v => prod (fun i => v (Fin.castSucc i)) * v (Fin.last _)
