toLinear — Mathlib

English

Each weight χ is a linear functional on L, i.e., χ ∈ L^∗, so weights act by scalars on weight spaces.

Русский

Каждый вес χ является линейным функционалом на L, то есть χ ∈ L^∗; веса задают скаляры на весовых пространствах.

LaTeX

$$$\\chi \\colon L \\to R$ является линейным отображением, т.е. $\\chi \\in L^{*}$.$$

Lean4

/-- A weight of a Lie module, bundled as a linear map. -/
@[simps]
def toLinear : L →ₗ[R] R where
  toFun := χ
  map_add' := LinearWeights.map_add χ χ.genWeightSpace_ne_bot
  map_smul' := LinearWeights.map_smul χ χ.genWeightSpace_ne_bot

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