English
Pairing relations hold for left and right placements: pairingIn_left and pairingIn_right express the same inner-product relations for short and long roots.
Русский
Отношения парирования справедливы слева и справа: pairingIn_left и pairingIn_right выражают одни и те же отношения по внутреннему произведению для коротких и длинных корней.
LaTeX
$$$P.pairingIn_\mathbb{Z}(short P, long P) = -1$ and related symmetry$$
Lean4
@[simp]
theorem pairingIn_twoShortAddLong_left :
P.pairingIn ℤ (twoShortAddLong P) i = 2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i :=
by
suffices P.pairing (twoShortAddLong P) i = 2 * 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 [twoShortAddLongRoot_eq, mul_add, add_mul, B.two_mul_apply_root_root]
ring
