English
If the root k equals the sum of roots i and j, then the height of k equals the sum of the heights of i and j.
Русский
Если корень k равен сумме корней i и j, то высота k равна сумме высот i и j.
LaTeX
$$$P.root\ k = P.root\ i + P.root\ j \;\Rightarrow\; b.height\ k = b.height\ i + b.height\ j$$$
Lean4
theorem height_add {i j k : ι} (hk : P.root k = P.root i + P.root j) : b.height k = b.height i + b.height j :=
by
obtain ⟨f, -, -, hf⟩ := b.exists_root_eq_sum_int i
obtain ⟨g, -, -, hg⟩ := b.exists_root_eq_sum_int j
have hfg : P.root k = ∑ l ∈ b.support, (f + g) l • P.root l := by
simp_rw [Pi.add_apply, add_smul, Finset.sum_add_distrib, ← hf, ← hg, hk]
simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, ← Finset.sum_add_distrib, Pi.add_apply]
