Zulip Chat Archive

Stream: Is there code for X?

Topic: vector.prod


view this post on Zulip 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

view this post on Zulip 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