exists_le_prime_notMem_of_isIdempotentElem

English

If a is idempotent and not in I, there exists a prime p containing I with a not in p.

Русский

Если a idempotent и a не принадлежит I, существует prime p, содержащий I, но не содержащий a.

LaTeX

$$$\\exists p:\\; p.IsPrime \\land I \\le p \\land a \\notin p.$$$

Lean4

theorem exists_le_prime_notMem_of_isIdempotentElem (a : α) (ha : IsIdempotentElem a) (haI : a ∉ I) :
    ∃ p : Ideal α, p.IsPrime ∧ I ≤ p ∧ a ∉ p :=
  have : Disjoint (I : Set α) (Submonoid.powers a) :=
    Set.disjoint_right.mpr <| by
      rw [ha.coe_powers]
      rintro _ (rfl | rfl)
      exacts [I.ne_top_iff_one.mp (ne_of_mem_of_not_mem' Submodule.mem_top haI).symm, haI]
  have ⟨p, h1, h2, h3⟩ := exists_le_prime_disjoint _ _ this
  ⟨p, h1, h2, Set.disjoint_right.mp h3 (Submonoid.mem_powers a)⟩

Похожие утверждения