exists_mem_pow_notMem_pow_succ

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

URI: https://scilib.ai/kg/mathlib#Ideal.exists_mem_pow_notMem_pow_succ

← MathLib Explorer

English

For each e, there exists x ∈ I^e with x ∉ I^{e+1}.

Русский

Для каждого e существует x ∈ I^e и x ∉ I^{e+1}.

LaTeX

$$$\exists x \in I^{e} \setminus I^{e+1}$$$

Lean4

theorem exists_mem_pow_notMem_pow_succ (I : Ideal A) (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (e : ℕ) :
    ∃ x ∈ I ^ e, x ∉ I ^ (e + 1) :=
  SetLike.exists_of_lt (I.pow_right_strictAnti hI0 hI1 e.lt_succ_self)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru