isRadical_bot

Mathlib.RingTheory.Ideal.Operations

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

English

If R is reduced, then the bottom ideal is radical.

Русский

Если R редуцировано, то ноль как идеал радикален.

LaTeX

$$$[IsReduced(R)] \\Rightarrow (\\perp).IsRadical$$$

Lean4

theorem isRadical_bot [IsReduced R] : (⊥ : Ideal R).IsRadical := by rwa [Ideal.isRadical_bot_iff]

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

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

Разделы

Аффилиация

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