English
The nodup property of allRoots is preserved under the map from allCoeffs to shortRoot/longRoot combinations.
Русский
Свойство без повторов allRoots сохраняется под отображением коэффициентов в комбинации корней shortRoot/longRoot.
LaTeX
$$allRoots_nodup(P) ↔ nodup(map_from_allCoeffs(P))$$
Lean4
@[simp]
theorem pairingIn_shortAddLong_right :
P.pairingIn ℤ i (shortAddLong P) = P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P) :=
by
suffices P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * 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 (shortAddLong P))
calc
P.pairing i (shortAddLong P) * B.form (P.root (shortAddLong P)) (P.root (shortAddLong P))
_ = 2 * B.form (P.root i) (shortAddLongRoot P) := ?_
_ = 2 * B.form (P.root i) (shortRoot P) + 2 * B.form (P.root i) (longRoot P) := ?_
_ =
P.pairing i (short P) * B.form (shortRoot P) (shortRoot P) +
P.pairing i (long P) * B.form (longRoot P) (longRoot P) :=
?_
_ = (P.pairing i (short P) + 3 * P.pairing i (long P)) * B.form (shortAddLongRoot P) (shortAddLongRoot P) := ?_
· rw [B.two_mul_apply_root_root]
· rw [shortAddLongRoot_eq, map_add, mul_add]
· rw [B.two_mul_apply_root_root, B.two_mul_apply_root_root]
· rw [long_eq_three_mul_short, shortAddLongRoot_shortRoot]; ring
