ker_subschemeι

Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι

English

The map I.subschemeι.app U is surjective.

Русский

Отображение I.subschemeι.app U является сюръективным.

LaTeX

$$Now, I.subschemeι.app U is surjective.$$

Lean4

@[simp]
theorem ker_subschemeι : I.subschemeι.ker = I := by ext; simp [ker_subschemeι_app]

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

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

Разделы

Аффилиация

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