coreflection

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

The image of the coroot set under coreflection i equals the coroot range.

Русский

Образ множества коротов под действием coreflection i равен диапазону коротов.

LaTeX

$$$ P.coreflection(i)''(range(P.coroot)) = range(P.coroot) $$$

Lean4

/-- The reflection associated to a coroot. -/
def coreflection : N ≃ₗ[R] N :=
  Module.reflection (P.root_coroot_two i)

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

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

Разделы

Аффилиация

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