reflection_apply_right

Mathlib.LinearAlgebra.RootSystem.Defs

URI: https://scilib.ai/kg/mathlib#RootPairing.IsOrthogonal.reflection_apply_right

English

If IsOrthogonal j i, then reflection j fixes root i as well: P.reflection j (P.root i) = P.root i.

Русский

Если IsOrthogonal j i, то reflection j также фиксирует корень i.

LaTeX

$$$$ P.reflection_j( P.root_i ) = P.root_i. $$$$

Lean4

theorem reflection_apply_right (h : IsOrthogonal P j i) : P.reflection j (P.root i) = P.root i :=
  h.symm.reflection_apply_left

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

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

Разделы

Аффилиация

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