instLinearLocalizationQ

Mathlib.CategoryTheory.Localization.Linear

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.instLinearLocalizationQ

English

An analogous linear structure exists for the Q'-localization as for localization with respect to W.

Русский

Аналогичная линейная структура существует и для локализации Q' по отношению к W.

LaTeX

$$$\text{Linear}_R(W.Q')$$$

Lean4

noncomputable instance : Functor.Linear R W.Q :=
  Localization.functor_linear R W.Q W

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

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

Разделы

Аффилиация

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