const_one

Mathlib.AlgebraicGeometry.StructureSheaf

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.StructureSheaf.const_one

English

The constant section with f = g = 1 yields the unit element.

Русский

Константная секция с f = g = 1 даёт единицу.

LaTeX

$$$ const_R 1 1 U hg = 1 $$$

Lean4

theorem const_one (U) : (const R 1 1 U fun _ _ => Submonoid.one_mem _) = 1 :=
  const_self R 1 U _

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

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

Разделы

Аффилиация

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