instLinearId

Mathlib.CategoryTheory.Linear.LinearFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instLinearId

English

The identity functor 𝟭_C carries an intrinsic linear structure over R, making it a linear functor.

Русский

Функтор идентичности 𝟭_C обладает линейной структурой над R и является линейным функтором.

LaTeX

$$$\\text{Linear } R (\\mathbf{1}_C).$$$

Lean4

instance : Linear R (𝟭 C) where

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

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

Разделы

Аффилиация

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