Commit 2020-07-07 15:15 11ba6873

View on Github →

chore(algebra/big_operators): use proper *_with_zero class in prod_eq_zero(_iff) (#3303) Also add a missing instance comm_semiring → comm_monoid_with_zero.

Estimated changes

Modified src/algebra/big_operators.lean

Modified src/algebra/ring.lean

Modified src/data/support.lean

added theorem function.mem_support

modified theorem function.support_prod

added theorem function.support_prod_subset