support_nilradical

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

English

For any I, I ≤ radical(I).

Русский

Для любого I, I содержится в радикале(I).

LaTeX

$$I ≤ I.radical$$

Lean4

@[simp]
theorem _root_.AlgebraicGeometry.Scheme.support_nilradical (X : Scheme.{u}) : X.nilradical.support = ⊤ :=
  rfl

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

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

Разделы

Аффилиация

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