English
For any i, the height b.height i is nonzero under CharZero assumptions and root-system crystallographic conditions; otherwise one derives a contradiction from the root-sum representations.
Русский
Для любого i высота b.height i не равна нулю при CharZero и кристаллографических условиях; иначе получаем противоречие из разложения по корням.
LaTeX
$$b.height i ≠ 0$$
Lean4
theorem height_ne_zero (i : ι) : b.height i ≠ 0 :=
by
obtain ⟨f, hf₀, hf₁, hf₂⟩ := b.exists_root_eq_sum_int i
rw [height_eq_sum hf₂]
rcases hf₁ with pos | neg
· refine (Finset.sum_pos' (fun i _ ↦ pos.le i) ?_).ne'
by_contra! contra
replace contra (j : ι) : f j = 0 := by
by_cases hj : j ∈ f.support
· exact le_antisymm (contra j (hf₀ hj)) (pos.le j)
· simpa using hj
exact P.ne_zero i <| by simp [hf₂, contra]
· refine (Finset.sum_neg' (fun i _ ↦ neg.le i) ?_).ne
by_contra! contra
replace contra (j : ι) : f j = 0 := by
by_cases hj : j ∈ f.support
· exact le_antisymm (neg.le j) (contra j (hf₀ hj))
· simpa using hj
exact P.ne_zero i <| by simp [hf₂, contra]
