rootSpanMem_reflectionPerm_self — Mathlib

English

ReflectionPerm preserves root-related pairings up to sign via pairingIn and algebra maps.

Русский

Отражение сохраняет пары корней с поправкой на знак через pairingIn и отображения алгебраических карт.

LaTeX

$$$P.pairingIn\;S\;j\;(P.reflectionPerm\;i\;k) = P.pairingIn\;S\;(P.reflectionPerm\;i\;j)\;k$$$

Lean4

theorem rootSpanMem_reflectionPerm_self [Module S M] (i : ι) :
    P.rootSpanMem S (P.reflectionPerm i i) = -P.rootSpanMem S i := by ext; simp

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