English
Let P be as above. The integer-valued pairing with threeShortAddLong P satisfies P.pairingIn ℤ (threeShortAddLong P) i = 3 · P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i.
Русский
Пусть P как выше. Сопряжение в ℤ на троекоротному-длинному корню даёт: P.pairingIn ℤ (threeShortAddLong P) i = 3 · P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i.
LaTeX
$$$P\,\mathrm{pairingIn}\,\mathbb{Z}\,(threeShortAddLong P)\, i = 3\,P\,\mathrm{pairingIn}\,\mathbb{Z}\,(short P)\, i + P\,\mathrm{pairingIn}\,\mathbb{Z}\,(long P)\, i$$$
Lean4
@[simp]
theorem pairingIn_threeShortAddLong_left :
P.pairingIn ℤ (threeShortAddLong P) i = 3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i :=
by
suffices P.pairing (threeShortAddLong P) i = 3 * P.pairing (short P) i + 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 [threeShortAddLongRoot_eq, mul_add, B.two_mul_apply_root_root, mul_left_comm (2 : R) (3 : R)]
ring
