nilradical_eq_zero

Mathlib.RingTheory.Nilpotent.Lemmas

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

English

If R is reduced (has no nonzero nilpotents), then nilradical(R) = 0.

Русский

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

LaTeX

$$nilradical R = 0$$

Lean4

@[simp]
theorem nilradical_eq_zero (R : Type*) [CommSemiring R] [IsReduced R] : nilradical R = 0 :=
  Ideal.ext fun _ => isNilpotent_iff_eq_zero

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

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

Разделы

Аффилиация

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