English
There exists a natural-valued coefficient function f with support in b.support such that P.root i equals either the sum ∑ f j • P.root j or its negation.
Русский
Существует функция f: ι → ℕ с опорой в b.support, такая что P.root i равен сумме ∑ f j • P.root j или её отрицанию.
LaTeX
$$Exists f : ι → ℕ, f.support ⊆ b.support ∧ (P.root i = ∑ j ∈ b.support, f j • P.root j ∨ P.root i = -∑ j ∈ b.support, f j • P.root j)$$
Lean4
theorem height_eq_sum {i : ι} {f : ι → ℤ} (heq : P.root i = ∑ j ∈ b.support, f j • P.root j) :
b.height i = ∑ j ∈ b.support, f j :=
by
suffices ∀ j ∈ b.support, (b.exists_root_eq_sum_int i).choose j = f j from Finset.sum_congr rfl this
intro j hj
obtain ⟨-, -, h⟩ := (b.exists_root_eq_sum_int i).choose_spec
rw [h, b.support.sum_subtype (p := (· ∈ b.support)) (by simp) (F := inferInstance),
b.support.sum_subtype (p := (· ∈ b.support)) (by simp) (F := inferInstance)] at heq
have aux (j : b.support) :=
Fintype.linearIndependent_iffₛ.mp (b.linearIndepOn_root.restrict_scalars' ℤ)
((b.exists_root_eq_sum_int i).choose ∘ (↑)) (f ∘ (↑)) (by simpa) j
simpa using aux ⟨j, hj⟩
