weylGroup

Mathlib.LinearAlgebra.RootSystem.WeylGroup

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

← MathLib Explorer

English

The ith reflection is an element of the Weyl group.

Русский

Отражение i-е является элементом группы Вейля.

LaTeX

$$$ \\text{reflection } P i \\in P.weylGroup $$$

Lean4

/-- The `Weyl group` of a root pairing is the group of automorphisms of the root pairing generated
by reflections. -/
def weylGroup : Subgroup (Aut P) :=
  Subgroup.closure (range (Equiv.reflection P))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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