instLinearLocalization'

Mathlib.CategoryTheory.Localization.Linear

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

English

There is a Linear R-structure on the localization regarding the prime version W.Localization'.

Русский

Для локализации W.Localization' существует линейная по R структура.

LaTeX

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

Lean4

noncomputable instance : Linear R W.Localization' :=
  Localization.linear R W.Q' W

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

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

Разделы

Аффилиация

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