## Stream: Is there code for X?

### Topic: prime generator of prime ideal

#### Julien Marquet (Feb 08 2021 at 21:33):

I wrote the theorem that states that the generator of a (principal) prime ideal is prime.
Should this go to matlib ? Are there things to add to this ?

import ring_theory.ideal.basic
import ring_theory.principal_ideal_domain

theorem submodule.is_principal.prime_generator_of_prime {α} [comm_ring α] (I: ideal α)
[submodule.is_principal I] [is_prime: ideal.is_prime I] (ne_bot: I ≠ ⊥):
prime (submodule.is_principal.generator I) :=
⟨
by {
intro h,
rw ← submodule.is_principal.eq_bot_iff_generator_eq_zero I at h,
exact ne_bot h,
},
by {
intro h,
have p₁: I = ⊤,
from ideal.eq_top_of_is_unit_mem I (submodule.is_principal.generator_mem I) h,
exact is_prime.1 p₁,
},
by {
simp only [← submodule.is_principal.mem_iff_generator_dvd I],
exact is_prime.2,
}
⟩


#### Patrick Massot (Feb 08 2021 at 21:36):

I have no idea whether we already have that. But if not then the process will be a lot smoother if you read https://leanprover-community.github.io/contribute/index.html, especially the style guide.

#### Anne Baanen (Feb 09 2021 at 10:19):

Looks like mathlib doesn't have this exact statement, although docs#ideal.span_singleton_prime should get you most of the way there. The only thing that I would also add before making this PR is the converse statement, turning the result into an iff.

Last updated: May 07 2021 at 21:10 UTC