mathlib3

2ea1650d - fix(algebra/ordered_monoid): slay with_top monoid diamonds caused by irreducibility (#8926)

fix(algebra/ordered_monoid): slay with_top monoid diamonds caused by irreducibility (#8926) https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Diamond.20in.20instances.20on.20.60with_top.20R.60 Instead of copying over from `with_zero`, just work through the definitions directly.