one_le_chainBotCoeff_of_root_add_mem

English

The chain bottom coefficient is given by the supremum over a set determined by the negated zsmul of i and j; it equals the maximum q such that certain linear relations hold for P.root additions.

Русский

Цепной нижний коэффициент задаётся сверху через наибольшую q, удовлетворяющую линейным отношениям, связанным с P.root и zsmul.

LaTeX

$$chainBotCoeff i j = sup { q | ... }$$

Lean4

theorem one_le_chainBotCoeff_of_root_add_mem [P.IsReduced] (h : P.root i - P.root j ∈ range P.root) :
    1 ≤ P.chainBotCoeff i j := by
  have h' := P.linearIndependent_of_sub_mem_range_root' h
  rwa [← root_sub_nsmul_mem_range_iff_le_chainBotCoeff h', one_smul, ← neg_mem_range_root_iff, neg_sub]

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