mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(Data/Nat/Prime): add 2 theorems

Open casavaca opened this issue 1 year ago • 2 comments
trafficstars

We have 2 exists_dvd_of_not_prime, but not the other way round. I found these 2 theorems useful when proving a number is not a prime number.

Open in Gitpod

casavaca avatar Mar 24 '24 00:03 casavaca