instCoeLinearMap

Mathlib.Algebra.Lie.Weights.Linear

URI: https://scilib.ai/kg/mathlib#LieModule.Weight.instCoeLinearMap

English

A weight χ is realized as a linear map L → R, i.e., χ is a linear functional on L.

Русский

Вес χ реализуется как линейное отображение L → R, то есть χ — линейный функционал на L.

LaTeX

$$$χ \\in \\mathrm{Hom}_R(L, R) = L^{*}.$$$

Lean4

instance instCoeLinearMap : CoeOut (Weight R L M) (L →ₗ[R] R) where coe := Weight.toLinear R L M

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

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

Разделы

Аффилиация

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