Prime ideals of Z are maximal

Stream: new members

[Alistair Bill]

Hello all,

Kevin and I were having problems proving the following two facts about ideals of Z (which hopefully should be an exercise in navigating the API for PIDs) - I wonder if anyone has any ideas?

example (p : ℕ) (hp : p.prime) : irreducible (p : ℤ) := sorry

example (r : ℤ) (hr : irreducible r) : ideal.is_maximal (ideal.span ({r} : set ℤ)) := sorry

Thanks

[Eric Rodriguez]

import ring_theory.int.basic

example (p : ℕ) (hp : p.prime) : irreducible (p : ℤ) := (nat.prime_iff_prime_int.mp hp).irreducible

example (r : ℤ) (hr : irreducible r) : ideal.is_maximal (ideal.span ({r} : set ℤ)) :=
principal_ideal_ring.is_maximal_of_irreducible hr