instLinearLocalization'Q'

Mathlib.CategoryTheory.Localization.Linear

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.instLinearLocalization'Q'

English

There is a linear structure for the Q'-localization as well.

Русский

Существует линейная структура и для локализации Q' к W.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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