Commit 2021-04-14 23:14 4605b55d
View on Github →feat(algebra/big_operators/finprod): add a few lemmas (#7130)
- add
finprod_nonneg
,finprod_cond_nonneg
, andfinprod_eq_zero
; - use
α → Prop
instead ofset α
infinprod_mem_eq_prod_of_mem_iff
, rename tofinprod_cond_eq_prod_of_cond_iff
.