one

Mathlib.GroupTheory.OreLocalization.Basic

URI: https://scilib.ai/kg/mathlib#OreLocalization.one

← MathLib Explorer

English

The unit element in the Ore localization is defined as 1 /ₒ 1.

Русский

Единичный элемент локализации Оре задаётся как 1 /ₒ 1.

LaTeX

$$$ 1_{R[S^{-1}]} = 1 /ₒ 1 $$$

Lean4

/-- `1` in the localization, defined as `1 /ₒ 1`. -/
@[to_additive (attr := irreducible) /-- `0` in the additive localization, defined as `0 -ₒ 0`. -/
    ]
protected def one : R[S⁻¹] :=
  1 /ₒ 1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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