Zulip Chat Archive

Stream: Is there code for X?

Topic: prime generator of prime ideal

view this post on Zulip 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,

view this post on Zulip 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.

view this post on Zulip 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