Dear list,
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
lemma sum_image_le:
fixes g :: "'a ⇒ 'b::ordered_com
Sounds good to me!
Larry
> On 28 Sep 2018, at 14:00, Alexander Maletzky
> 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
> accordin