mathlib

bfadf057 - feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (#4766)