pairingIn_reflectionPerm_self_right

English

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

Русский

Аналогично, P.pairingIn S i (P.reflectionPerm j j) = − P.pairingIn S i j.

LaTeX

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

Lean4

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

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