mathlib3
c7c40a7d - feat(*/pi): add lemmas about how `single` interacts with operators (#6317)

Commit

4 years ago

feat(*/pi): add lemmas about how `single` interacts with operators (#6317) This also adds a missing pi instances for `monoid_with_zero`.

Author

eric-wieser

Parents