weylGroupToPerm — Mathlib

English

The permutation representation of the Weyl group has image equal to the closure of the reflections range.

Русский

Перестановочное представление Weyl-группы имеет образ, равный замыканию образа отражений.

LaTeX

$$$P.weylGroupToPerm.range = \\operatorname{Subgroup.closure}(\\operatorname{range}(P.reflectionPerm)).$$$

Lean4

/-- The permutation representation of the Weyl group induced by `reflectionPerm`. -/
abbrev weylGroupToPerm :=
  (Equiv.indexHom P).restrict P.weylGroup

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