height_one_of_mem_support — Mathlib

English

If i belongs to the support of the base, then the height of i is equal to 1.

Русский

Если i принадлежит поддержке основы, то высота i равна 1.

LaTeX

$$$i \in b_{\mathrm{support}} \quad \Rightarrow \quad b.height(i) = 1$$$

Lean4

theorem height_one_of_mem_support {i : ι} (hi : i ∈ b.support) : b.height i = 1 := by
  classical
  have : P.root i = ∑ j ∈ b.support, (Pi.single i 1 : ι → ℤ) j • P.root j := by
    rw [Finset.sum_eq_single_of_mem i hi (by simp_all)]; simp
  simpa [height_eq_sum this]

Похожие утверждения