bijOn_coreflection_coroot

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

The coreflection i induces a bijection on the coroot range.

Русский

Корефлексия i задаёт биективное отображение на диапазоне коротов.

LaTeX

$$$ BijOn(P.coreflection(i), range(P.coroot), range(P.coroot)) $$$

Lean4

theorem bijOn_coreflection_coroot : BijOn (P.coreflection i) (range P.coroot) (range P.coroot) :=
  bijOn_reflection_root P.flip i

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

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

Разделы

Аффилиация

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