Zulip Chat Archive

Stream: new members

Topic: Prime ideals of Z are maximal


Alistair Bill (Sep 28 2022 at 10:44):

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 (Sep 28 2022 at 11:02):

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

Last updated: Dec 20 2023 at 11:08 UTC