[isabelle-dev] Lemma "sum_image_le"

[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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20181006/25c7e510/attachment.p7s>