chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx

English

A relation expresses that the pairing of the chainTopIdx yields a certain integer in the root pairing.

Русский

Связь цепи topIdx выражает, что пара корней через chainTopIdx сопоставляет целое число в pairing.

LaTeX

$$$$ P.chainTopCoeff i j + P.chainBotCoeff i j = P.pairingIn \mathbb{Z} (P.chainTopIdx i j) i $$$$

Lean4

theorem chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx :
    P.chainBotCoeff i j + P.chainTopCoeff i j = P.pairingIn ℤ (P.chainTopIdx i j) i :=
  by
  replace h : LinearIndependent R ![P.root i, P.root (P.chainTopIdx i j)] := by
    rwa [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul, LinearIndependent.pair_add_smul_right_iff]
  calc
    (P.chainBotCoeff i j + P.chainTopCoeff i j : ℤ)
    _ = P.chainBotCoeff i (P.chainTopIdx i j) := by simp
    _ = P.chainBotCoeff i (P.chainTopIdx i j) - P.chainTopCoeff i (P.chainTopIdx i j) := by simp
    _ = P.pairingIn ℤ (P.chainTopIdx i j) i := by rw [P.chainBotCoeff_sub_chainTopCoeff h]

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