isRadical_bot_iff

Mathlib.RingTheory.Ideal.Operations

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

← MathLib Explorer

English

The bottom ideal is radical iff the ring is reduced.

Русский

Нижний идеал радикален тогда и только тогда, когда кольцо редуцировано.

LaTeX

$$$(\\perp).IsRadical \\iff IsReduced(R)$$$

Lean4

theorem isRadical_bot_iff : (⊥ : Ideal R).IsRadical ↔ IsReduced R := by
  simp only [IsRadical, SetLike.le_def, Ideal.mem_radical_iff, Ideal.mem_bot, forall_exists_index, isReduced_iff,
    IsNilpotent]

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

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

Разделы

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

Аффилиация

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