## Stream: Is there code for X?

### Topic: vector.prod

#### Kevin Buzzard (Sep 01 2020 at 11:45):

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 (Sep 01 2020 at 11:57):

aah I see it's just list.prod

Last updated: May 17 2021 at 15:13 UTC