Add a couple lemmas about product in Data.List.Properties

agda / agda-stdlib

The Agda standard library

https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary

Other

585 stars 237 forks source link

Add a couple lemmas about product in Data.List.Properties #2460

Closed dolio closed 3 months ago

dolio commented 3 months ago

These are a couple of lemmas I found useful when trying to formalize Euclid's proof of the infinitude of primes.

the product of non-zero naturals is non-zero
any element of a list of non-zero naturals is less-or-equal to the product of the list

Hopefully I didn't just miss these somewhere else, but the divisibility result above this was about the only theorem I could find about product.

jamesmckinna commented 3 months ago

And: CHANGELOG entries please!

jamesmckinna commented 3 months ago

NB. It looks as though you have forked the main repo and then done this PR directly on your master branch... it's much better (cleaner; more robust; easier to handle mutliple PRs simultaneously) to do PRs independently on separate branches off your master branch... as described in section 5 of HACKING...

jamesmckinna commented 3 months ago

Thanks for a very nice first PR! (NB better to fix up your git branches before the next one... ;-)) A couple of final refinements, and we should be good to go! @JacquesCarette are you happy with the refactoring?