mem_radical_of_pow_mem

Mathlib.RingTheory.Ideal.Operations

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

English

If x^m is in radical I, then x is in radical I.

Русский

Если x^m принадлежит радикалу I, то x принадлежит радикалу I.

LaTeX

$$$x^{m} \\in \\operatorname{radical}(I) \\Rightarrow x \\in \\operatorname{radical}(I)$$$

Lean4

theorem mem_radical_of_pow_mem {I : Ideal R} {x : R} {m : ℕ} (hx : x ^ m ∈ radical I) : x ∈ radical I :=
  radical_idem I ▸ ⟨m, hx⟩

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

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

Разделы

Аффилиация

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