English
For all i, the integer-valued pairing with threeShortAddLong P satisfies P.pairingIn ℤ (threeShortAddLong P) i = 3 · P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i.
Русский
Для всех i: 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_right :
P.pairingIn ℤ i (threeShortAddLong P) = P.pairingIn ℤ i (short P) + P.pairingIn ℤ i (long P) :=
by
suffices P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P) 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 <| threeShortAddLong P)
calc
P.pairing i (threeShortAddLong P) * B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P)
_ = 2 * B.form (P.root i) (threeShortAddLongRoot P) := ?_
_ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * B.form (P.root i) (longRoot P) := ?_
_ =
P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
P.pairing i (long P) * B.form (longRoot P) (longRoot P) :=
?_
_ = (P.pairing i (short P) + P.pairing i (long P)) * B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P) :=
?_
· rw [B.two_mul_apply_root_root]
· rw [threeShortAddLongRoot_eq, map_add, mul_add, map_smul, smul_eq_mul]; ring
· rw [B.two_mul_apply_root_root, B.two_mul_apply_root_root, long_eq_three_mul_short]; ring
· rw [threeShortAddLongRoot_longRoot]; ring
