nilradical_eq_bot

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.nilradical_eq_bot

English

If X is reduced, its nilradical is the bottom element.

Русский

Если X приведена, её нилрадикал равен нулю.

LaTeX

$$[IsReduced X] ⇒ X.nilradical = \\bot$$

Lean4

theorem nilradical_eq_bot [IsReduced X] : X.nilradical = ⊥ := by ext;
  simp [nilradical, Ideal.radical_eq_iff.mpr (Ideal.isRadical_bot)]

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

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

Разделы

Аффилиация

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