zero_isRadical_iff

Mathlib.RingTheory.Nilpotent.Basic

URI: https://scilib.ai/kg/mathlib#zero_isRadical_iff

← MathLib Explorer

English

In a monoid with zero, 0 is radical iff the ring is reduced.

Русский

В кольце с нулём 0 радикален тогда и только тогда, когда кольцо редуцировано.

LaTeX

$$$\\text{IsRadical}(0) \\iff \\text{IsReduced }R$$$

Lean4

theorem zero_isRadical_iff [MonoidWithZero R] : IsRadical (0 : R) ↔ IsReduced R :=
  by
  simp_rw [isReduced_iff, IsNilpotent, exists_imp, ← zero_dvd_iff]
  exact forall_swap

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

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

Разделы

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

Аффилиация

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