nilradical_eq_bot_iff

Mathlib.RingTheory.Nilpotent.Lemmas

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

← MathLib Explorer

English

Nilradical equals the bottom ideal if and only if the ring is reduced.

Русский

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

LaTeX

$$nilradical R = ⊥ ↔ IsReduced R$$

Lean4

theorem nilradical_eq_bot_iff {R : Type*} [CommSemiring R] : nilradical R = ⊥ ↔ IsReduced R := by
  simp_rw [eq_bot_iff, SetLike.le_def, Submodule.mem_bot, mem_nilradical, isReduced_iff]

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

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

Разделы

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

Аффилиация

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