reflection_apply

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

For any i ∈ ι and x ∈ M, the reflection acts by subtracting the scalar (P.coroot' i x) times the i-th root from x.

Русский

Для любого i ∈ ι и любого x ∈ M отражение действует так: x ↦ x − (P.coroot' i x) · P.root i.

LaTeX

$$$ P.reflection(i)(x) = x - (P.coroot'(i)\,x) \cdot P.root(i) $$$

Lean4

theorem reflection_apply (x : M) : P.reflection i x = x - (P.coroot' i x) • P.root i :=
  rfl

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

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

Разделы

Аффилиация

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