instOne

Mathlib.GroupTheory.OreLocalization.Basic

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

English

There is a canonical One instance for the Ore localization, aligning with the usual multiplicative identity.

Русский

Существует канонический элемент единицы для локализации Оре, согласованный с обычной единицей умножения.

LaTeX

$$$\text{One} (R[S^{-1}])$$$

Lean4

@[to_additive]
instance : One R[S⁻¹] :=
  ⟨OreLocalization.one⟩

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

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

Разделы

Аффилиация

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