reflection_image_eq

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

The map coreflection i induces a bijection on the coroot range.

Русский

Отображение coreflection i задаёт биективное отображение на диапазоне коротов.

LaTeX

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

Lean4

@[simp]
theorem reflection_image_eq : P.reflection i '' (range P.root) = range P.root :=
  (P.bijOn_reflection_root i).image_eq

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

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

Разделы

Аффилиация

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