English
Let P be as above. Then for all i, P.pairingIn ℤ (threeShortAddTwoLong P) i = 3 · P.pairingIn ℤ (short P) i + 2 · P.pairingIn ℤ (long P) i.
Русский
Пусть P как выше. Тогда для всех i: P.pairingIn ℤ (threeShortAddTwoLong P) i = 3 · P.pairingIn ℤ (short P) i + 2 · P.pairingIn ℤ (long P) i.
LaTeX
$$$P\\,\\mathrm{pairingIn}\\,\\{\\mathbb{Z}\\} (threeShortAddTwoLong P)\\, i = 3\\,P\\,\\mathrm{pairingIn}\\,\\{\\mathbb{Z}\\} (short P)\\, i + 2\\,P\\,\\mathrm{pairingIn}\\,\\{\\mathbb{Z}\\} (long P)\\, i$$$
Lean4
@[simp]
theorem pairingIn_threeShortAddTwoLong_left :
P.pairingIn ℤ (threeShortAddTwoLong P) i = 3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i :=
by
suffices P.pairing (threeShortAddTwoLong P) i = 3 * P.pairing (short P) i + 2 * P.pairing (long P) i from
algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_add, map_mul, map_ofNat]
have : Fintype ι := Fintype.ofFinite ι
have B := (P.posRootForm ℤ).toInvariantForm
apply mul_right_cancel₀ (B.ne_zero i)
rw [← B.two_mul_apply_root_root]
simp [threeShortAddTwoLongRoot_eq, mul_add, B.two_mul_apply_root_root, mul_left_comm _ (3 : R)]
ring
