mathlib
11ba6873 - chore(algebra/big_operators): use proper `*_with_zero` class in `prod_eq_zero(_iff)` (#3303)

Commit

5 years ago

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`.

Author

urkud

Parents

12c2acb8

mathlib 11ba6873 - chore(algebra/big_operators): use proper `*_with_zero` class in `prod_eq_zero(_iff)` (#3303)

mathlib
11ba6873 - chore(algebra/big_operators): use proper `*_with_zero` class in `prod_eq_zero(_iff)` (#3303)