pairingIn_reflectionPerm_self_left

English

For any i, j, P.pairingIn S (P.reflectionPerm i i) j = - P.pairingIn S i j.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem pairingIn_reflectionPerm_self_left [FaithfulSMul S R] [P.IsValuedIn S] (i j : ι) :
    P.pairingIn S (P.reflectionPerm i i) j = -P.pairingIn S i j := by
  simp [← (FaithfulSMul.algebraMap_injective S R).eq_iff]

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