radical_idem

Mathlib.RingTheory.Ideal.Operations

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

English

The radical operation is idempotent: applying it twice yields the same radical.

Русский

Операция радикала идемпотентна: применение дважды даёт тот же радикал.

LaTeX

$$$\\operatorname{radical}(\\operatorname{radical}(I)) = \\operatorname{radical}(I)$$$

Lean4

@[simp]
theorem radical_idem : radical (radical I) = radical I :=
  (radical_isRadical I).radical

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

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

Разделы

Аффилиация

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