isRadical_bot_of_noZeroDivisors

Mathlib.RingTheory.Ideal.Operations

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

← MathLib Explorer

English

In a ring with no zero divisors, the bottom ideal is radical.

Русский

В кольце без нулевых делителей нулевой идеал радикален.

LaTeX

$$$\\forall R [NoZeroDivisors R], (\\perp : Ideal R).IsRadical$$$

Lean4

theorem isRadical_bot_of_noZeroDivisors {R} [CommSemiring R] [NoZeroDivisors R] : (⊥ : Ideal R).IsRadical := fun _ hx =>
  hx.recOn fun _ hn => pow_eq_zero hn

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

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

Разделы

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

Аффилиация

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