Commit 2022-02-21 11:38 afcc7e74

View on Github →

feat(data/nat/prime): move nat.prime_iff_prime_int; add int.prime_two/three (#12133) I found it useful to have these results with somewhat lighter imports.

Estimated changes

Modified src/data/nat/prime.lean

added theorem int.prime_three

added theorem int.prime_two

added theorem nat.prime_iff_prime_int

Modified src/ring_theory/int/basic.lean

deleted theorem nat.prime_iff_prime_int