vector.prod

Stream: Is there code for X?

[Kevin Buzzard]

import tactic

def vector.prod {M : Type} [monoid M] (n : ℕ) : vector M n → M :=
nat.rec_on n (λ _, 1) (λ n Pn v, v.head * Pn (v.tail))
-- or is it Pn (v.tail) * v.head? Which comes first, heads or tails? All I remember is a picture of Wiggler lol

[Kevin Buzzard]

aah I see it's just list.prod