ofIdx

Mathlib.LinearAlgebra.RootSystem.WeylGroup

URI: https://scilib.ai/kg/mathlib#RootPairing.weylGroup.ofIdx

English

The ith reflection is represented as an element of the Weyl group via ofIdx i.

Русский

i-е отражение выражено как элемент группы Вейля через ofIdx i.

LaTeX

$$$ \\text{ofIdx}(i) \\in P.weylGroup $$$

Lean4

/-- The `ith` reflection as a term of the Weyl group. -/
def ofIdx (i : ι) : P.weylGroup :=
  ⟨_, P.reflection_mem_weylGroup i⟩

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

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

Разделы

Аффилиация

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