oreNum

Mathlib.GroupTheory.OreLocalization.OreSet

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

← MathLib Explorer

English

The Ore numerator is the numerator of the fraction in the Ore localization.

Русский

Числитель Оре — это числитель дроби в локализации Оре.

LaTeX

$$oreNum(r,s) = numerator of the fraction r/ₒ s$$

Lean4

/-- The Ore numerator of a fraction. -/
@[to_additive AddOreLocalization.oreMin /-- The Ore minuend of a difference. -/
    ]
def oreNum (r : R) (s : S) : R :=
  OreSet.oreNum r s

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

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

Разделы

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

Аффилиация

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