[isabelle-dev] Lemma "sum_image_le"

[Lawrence Paulson]

Sounds good to me!
Larry

> On 28 Sep 2018, at 14:00, Alexander Maletzky <alexander.maletzky at risc.jku.at> wrote:
> 
> 
> lemma "sum_image_le" in theory "Groups_Big", which is stated for
> type-class "ordered_ab_group_add", holds more generally for
> "ordered_comm_monoid_add" (proof below). May I propose to change it
> accordingly?
> 
> Best regards,
> Alexander

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180928/df679b7f/attachment-0002.html>