weylGroupCorootRep — Mathlib

English

The natural representation of the Weyl group on the coroot space is given by the opposite action on coroots.

Русский

Естественное представление Weyl-группы на пространстве коретов задаётся противоположным действием на короты.

LaTeX

$$$\\text{weylGroupCorootRep}: \\text{Representation}_{R}(P.weylGroup.op)\\ N$$$

Lean4

/-- The natural representation of the Weyl group on the coroot space. -/
def weylGroupCorootRep : Representation R P.weylGroup.op N :=
  Representation.ofDistribMulAction R P.weylGroup.op N

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