English
This lemma relates the bottom coefficient at the sum/difference of roots with the corresponding top coefficient: chainBotCoeff(i, chainTopIdx i, j) equals chainBotCoeff(i, j) plus chainTopCoeff(i, j).
Русский
Это соотношение связывает нижний коэффициент в отношении суммы/разности корней с соответствующим верхним коэффициентом: chainBotCoeff(i, chainTopIdx i, j) = chainBotCoeff(i, j) + chainTopCoeff(i, j).
LaTeX
$$$$ P.chainBotCoeff(i, P.chainTopIdx(i, j)) = P.chainBotCoeff(i, j) + P.chainTopCoeff(i, j) $$$$
Lean4
theorem chainCoeff_chainTopIdx_aux :
P.chainBotCoeff i (P.chainTopIdx i j) = P.chainBotCoeff i j + P.chainTopCoeff i j ∧
P.chainTopCoeff i (P.chainTopIdx i j) = 0 :=
by
have aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (P.chainTopIdx i j)] :=
by rw [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul, LinearIndependent.pair_add_smul_right_iff]
by_cases h : LinearIndependent R ![P.root i, P.root j]
swap; · simp [chainTopCoeff_of_not_linearIndependent, chainBotCoeff_of_not_linearIndependent, h]
have h' : LinearIndependent R ![P.root i, P.root (P.chainTopIdx i j)] := by rwa [← aux]
set S₁ : Set ℤ := {z | P.root j + z • P.root i ∈ range P.root} with S₁_def
set S₂ : Set ℤ := {z | P.root (P.chainTopIdx i j) + z • P.root i ∈ range P.root} with S₂_def
have hS₁₂ : S₂ = (fun z ↦ (-P.chainTopCoeff i j : ℤ) + z) '' S₁ := by ext;
simp [S₁_def, S₂_def, root_chainTopIdx, add_smul, add_assoc, natCast_zsmul]
have hS₁ : S₁ = Icc (-P.chainBotCoeff i j : ℤ) (P.chainTopCoeff i j) := by ext;
rw [S₁_def, mem_setOf_eq, root_add_zsmul_mem_range_iff h]
have hS₂ : S₂ = Icc (-P.chainBotCoeff i (P.chainTopIdx i j) : ℤ) (P.chainTopCoeff i (P.chainTopIdx i j)) := by ext;
rw [S₂_def, mem_setOf_eq, root_add_zsmul_mem_range_iff h']
rw [hS₁, hS₂, image_const_add_Icc, neg_add_cancel, Icc_eq_Icc_iff (by simp), neg_eq_iff_eq_neg, neg_add_rev, neg_neg,
neg_neg] at hS₁₂
norm_cast at hS₁₂
