tensoringLeft_linear

Mathlib.CategoryTheory.Monoidal.Linear

URI: https://scilib.ai/kg/mathlib#CategoryTheory.tensoringLeft_linear

English

Similarly, for any semiring R, the functor tensorRight X is R-linear.

Русский

Аналогично, для любого полускольного кольца R, тензоризация справа на X линейна над R.

LaTeX

$$$(X : C) \\;\\Rightarrow\\; \\text{Functor.Linear } R (\\text{tensorRight } X)$$$

Lean4

instance tensoringLeft_linear (X : C) : ((tensoringLeft C).obj X).Linear R where

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

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

Разделы

Аффилиация

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