pairing_reflectionPerm_self_right

English

For all i, j, the pairing with reflectionPerm(j,j) on the right equals the negation of the pairing: pairing i (reflectionPerm(j,j)) = - pairing i j.

Русский

Для всех i, j правая часть: pairing i (reflectionPerm(j,j)) = - pairing i j.

LaTeX

$$$ P.pairing(i, P.reflectionPerm(j,j)) = -P.pairing(i,j) $$$

Lean4

@[simp]
theorem pairing_reflectionPerm_self_right (i j : ι) : P.pairing i (P.reflectionPerm j j) = -P.pairing i j := by
  rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul, sub_add_cancel_left, map_neg,
    root_coroot_eq_pairing]

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