coreflection_image_eq

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coreflection_image_eq : P.coreflection i '' (range P.coroot) = range P.coroot :=
  (P.bijOn_coreflection_coroot i).image_eq

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

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

Разделы

Аффилиация

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