feat(data/nat/prime): prime.even_iff (#14688)
feat(data/nat/prime): prime.even_iff (#14688)

Adds a lemma saying that the only even prime is two.





leanprover-community/mathlib,leanprover-community/mathlib