pairing_reflectionPerm_self_left — Mathlib

English

For all i, j, the pairing with reflectionPerm(i,i) on the left yields the negative of pairing with i on the left: pairing(P.reflectionPerm(i,i), j) = - pairing(i, j).

Русский

Для всех i, j паринг с reflectionPerm(i,i) слева равен минусу паринга с i слева: pairing(reflectionPerm(i,i), j) = - pairing(i, j).

LaTeX

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

Lean4

@[simp]
theorem pairing_reflectionPerm_self_left (P : RootPairing ι R M N) (i j : ι) :
    P.pairing (P.reflectionPerm i i) j = -P.pairing i j := by
  rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul, sub_add_cancel_left,
    LinearMap.map_neg₂, root'_coroot_eq_pairing]

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