Commit 2021-11-06 09:47 239bf055
View on Github →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 ℕ.