instNegOreLocalization

Mathlib.RingTheory.OreLocalization.Basic

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

English

There is an instance providing a Neg structure on Ore localization.

Русский

Существует инстанс, задающий структуру Neg на локализации Оре.

LaTeX

$$instance : Neg (X[S^{-1}])$$

Lean4

instance instNegOreLocalization : Neg X[S⁻¹] :=
  ⟨OreLocalization.neg⟩

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

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

Разделы

Аффилиация

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