Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-20 09:48 568eb9b4

View on Github →

feat(data/nat/prime): add two lemmas (#17605) We add two easy lemmas. From flt-regular

Estimated changes

Modified src/data/nat/prime.lean

added theorem nat.prime.five_le_of_ne_two_of_ne_three

added theorem nat.prime.odd_of_ne_two