bijOn_reflection_root

Mathlib.LinearAlgebra.RootSystem.Defs

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

← MathLib Explorer

English

The coroot of a reflected coroot equals the coreflection of the coroot by i.

Русский

Корoot отражённого корота равен корефлекции корота по i.

LaTeX

$$$ P.coroot(P.reflectionPerm(i,j)) = (P.coreflection(i))(P.coroot(j)) $$$

Lean4

theorem bijOn_reflection_root : BijOn (P.reflection i) (range P.root) (range P.root) :=
  Module.bijOn_reflection_of_mapsTo _ <| P.mapsTo_reflection_root i

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

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

Разделы

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

Аффилиация

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