English
Let α be a type with multiplication. For any m and a: Fin m → α, the value of FinVec.prod a equals the product of the components a(i) over i ∈ Fin m, i.e. ∏_{i : Fin m} a(i).
Русский
Пусть α — множество с умножением. Для любого m и a: Fin m → α выполняется равенство FinVec.prod a = ∏_{i : Fin m} a(i).
LaTeX
$$$\\forall m\\, (a : \\mathrm{Fin}\,m \\to \\alpha),\\quad \\mathrm{FinVec.prod}\\,a = \\prod_{i : \\mathrm{Fin}\,m} a(i).$$$
Lean4
/-- This can be used to prove
```lean
example [CommMonoid α] (a : Fin 3 → α) : ∏ i, a i = a 0 * a 1 * a 2 :=
(prod_eq _).symm
```
-/
@[to_additive (attr := simp) /-- This can be used to prove
```lean
example [AddCommMonoid α] (a : Fin 3 → α) : ∑ i, a i = a 0 + a 1 + a 2 :=
(sum_eq _).symm
``` -/
]
theorem prod_eq [CommMonoid α] : ∀ {m} (a : Fin m → α), prod a = ∏ i, a i
| 0, _ => rfl
| 1, a => (Fintype.prod_unique a).symm
| n + 2, a => by rw [Fin.prod_univ_castSucc, prod, prod_eq]
