feat(data/list/basic): list products (#10184)
feat(data/list/basic): list products (#10184)

Adding a couple of lemmas about list products. The first is a simpler variant of `head_mul_tail_prod'` in the case where the list is not empty.  The other is a variant of `list.prod_ne_zero` for `list ℕ`.



Co-authored-by: Floris van Doorn <04eee3258902297ef5081ba8b0786f6ab1274795@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib