pairing_eq_add_of_root_eq_smul_add_smul

English

The pairing of a coroot and a root satisfies coroot-root equality: coroot-root equals 2 when i equals j.

Русский

Парирование коррота и корня удовлетворяет равенство коррото-рут: при i = j равняется 2.

LaTeX

$$$ P.toLinearMap.flip (P.coroot i) (P.root i) = 2 $$$

Lean4

theorem pairing_eq_add_of_root_eq_smul_add_smul {i j k l : ι} {x y : R} (h : P.root k = x • P.root i + y • P.root l) :
    P.pairing k j = x • P.pairing i j + y • P.pairing l j := by
  simp only [← root_coroot_eq_pairing, h, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply, smul_eq_mul]

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