prime generator of prime ideal

Stream: Is there code for X?

[Julien Marquet]

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]

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]

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.