pow_mem_iff_mem

Mathlib.RingTheory.Ideal.Prime

URI: https://scilib.ai/kg/mathlib#Ideal.IsPrime.pow_mem_iff_mem

← MathLib Explorer

English

If I is prime, then r^n ∈ I implies r ∈ I for n > 0.

Русский

Если I прост, то из r^n ∈ I следует r ∈ I при n > 0.

LaTeX

$$I.IsPrime \Rightarrow ∀ {r} {n}, 0 < n → r^{n} \in I \Rightarrow r \in I$$

Lean4

theorem pow_mem_iff_mem {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (hn : 0 < n) : r ^ n ∈ I ↔ r ∈ I :=
  ⟨hI.mem_of_pow_mem n, fun hr => I.pow_mem_of_mem hr n hn⟩

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

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

Разделы

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

Аффилиация

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