mem_radical_iff

Mathlib.RingTheory.Ideal.Operations

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

English

r ∈ I.radical iff ∃ n, r^n ∈ I.

Русский

r находится в радикале I тогда и только тогда, когда существует n: r^n ∈ I.

LaTeX

$$$$ r \in I.radical \iff \exists n \in \mathbb{N},\ r^n \in I $$$$

Lean4

theorem mem_radical_iff {r : R} : r ∈ I.radical ↔ ∃ n : ℕ, r ^ n ∈ I :=
  Iff.rfl

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

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

Разделы

Аффилиация

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