pairingIn_reflectionPerm — Mathlib

English

For any i, j, k, the root-pairing satisfies P.pairingIn S j (P.reflectionPerm i k) = P.pairingIn S (P.reflectionPerm i j) k.

Русский

Для любых i, j, k выполняется P.pairingIn S j (P.reflectionPerm i k) = P.pairingIn S (P.reflectionPerm i j) k.

LaTeX

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

Lean4

theorem pairingIn_reflectionPerm [FaithfulSMul S R] [P.IsValuedIn S] (i j k : ι) :
    P.pairingIn S j (P.reflectionPerm i k) = P.pairingIn S (P.reflectionPerm i j) k :=
  by
  simp only [← (FaithfulSMul.algebraMap_injective S R).eq_iff, algebraMap_pairingIn]
  exact pairing_reflectionPerm P i j k

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