English
For all i, the integer-valued pairing with threeShortAddTwoLong P satisfies P.pairingIn ℤ i (threeShortAddTwoLong P) = P.pairingIn ℤ i (short P) + 2 · P.pairingIn ℤ i (long P).
Русский
Для всех i: P.pairingIn ℤ i (threeShortAddTwoLong P) = P.pairingIn ℤ i (short P) + 2 · P.pairingIn ℤ i (long P).
LaTeX
$$$P\\,\\mathrm{pairingIn}\\,\\{\\mathbb{Z}\\} i (threeShortAddTwoLong P) = P\\.\\mathrm{pairingIn}\\,\\{\\mathbb{Z}\\} i (short P) + 2 \, P\\.\\mathrm{pairingIn}\\,\\{\\mathbb{Z}\\} i (long P)$$$
Lean4
@[simp]
theorem pairingIn_threeShortAddTwoLong_right :
P.pairingIn ℤ i (threeShortAddTwoLong P) = P.pairingIn ℤ i (short P) + 2 * P.pairingIn ℤ i (long P) :=
by
suffices P.pairing i (threeShortAddTwoLong P) = P.pairing i (short P) + 2 * 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 <| threeShortAddTwoLong P)
calc
P.pairing i (threeShortAddTwoLong P) * B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P)
_ = 2 * B.form (P.root i) (threeShortAddTwoLongRoot P) := ?_
_ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * (2 * B.form (P.root i) (longRoot P)) := ?_
_ =
P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
2 * P.pairing i (long P) * B.form (longRoot P) (longRoot P) :=
?_
_ =
(P.pairing i (short P) + 2 * P.pairing i (long P)) *
B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P) :=
?_
· rw [B.two_mul_apply_root_root]
· simp only [threeShortAddTwoLongRoot_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 [threeShortAddTwoLongRoot_longRoot]; ring
