root_add_zsmul_mem_range_iff — Mathlib

English

The Chain Top coefficient is the least upper bound of the zsmul-based set of root combinations; it equals the supremum of k for which P.root j + k•P.root i lies in the root range.

Русский

Коэффициент верхней цепи равен супремусу по всем комбинациям корня, образующим диапазон корня.

LaTeX

$$chainTopCoeff i j = sup { k | P.root j + k • P.root i ∈ range P.root }$$

Lean4

theorem root_add_zsmul_mem_range_iff {z : ℤ} :
    P.root j + z • P.root i ∈ range P.root ↔ z ∈ Icc (-P.chainBotCoeff i j : ℤ) (P.chainTopCoeff i j) :=
  by
  rcases z.eq_nat_or_neg with ⟨n, rfl | rfl⟩
  · simp [P.root_add_nsmul_mem_range_iff_le_chainTopCoeff h]
  · simp [P.root_sub_nsmul_mem_range_iff_le_chainBotCoeff h, ← sub_eq_add_neg]

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