mathlib3

427564e0 - chore(algebra/monoid_algebra): Fix TODO about unwanted unfolding (#4532)

chore(algebra/monoid_algebra): Fix TODO about unwanted unfolding (#4532) For whatever reason, supplying `zero` and `add` explicitly makes the proofs work inline. This TODO was added by @johoelzl in f09abb1c47a846c33c0e996ffa9bf12951b40b15.