English
If P.root k = P.root i + z·P.root j for an integer z, then height(k) = height(i) + z·height(j).
Русский
Если P.root k = P.root i + z·P.root j для целого z, тогда высота k равна высоте i плюс z умноженное на высоту j.
LaTeX
$$$P.root\ k = P.root\ i + z \cdot P.root\ j \Rightarrow b.height\ k = b.height\ i + z \cdot b.height\ j$$$
Lean4
theorem height_add_zsmul {i j k : ι} {z : ℤ} (hk : P.root k = P.root i + z • P.root j) :
b.height k = b.height i + z • 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 + z • g) l • P.root l := by
simp_rw [Pi.add_apply, Pi.smul_apply, add_smul, smul_assoc, Finset.sum_add_distrib, ← Finset.smul_sum, ← hf, ← hg,
hk]
simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, Pi.add_apply, Pi.smul_apply, Finset.sum_add_distrib,
Finset.smul_sum]
