[isabelle-dev] Lemma "sum_image_le"

[Alexander Maletzky]

Great, thanks!

Alexander


Am 06.10.2018 um 13:06 schrieb Tobias Nipkow:
> Since Alexander cannot push changes, I have done so now.
>
> Tobias
>
> On 28/09/2018 18:44, Lawrence Paulson wrote:
>> Sounds good to me!
>> Larry
>>
>>> On 28 Sep 2018, at 14:00, Alexander Maletzky
>>> <alexander.maletzky at risc.jku.at
>>> <mailto: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
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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