coeff_eq_zero_of_lt_lexOrder — Mathlib

English

If d is strictly less than the leading lex order of φ, then the coefficient at d vanishes: coeff(d, φ) = 0.

Русский

Если d строго меньше ведущего лексического порядка φ, то коэффициент при d равен нулю.

LaTeX

$$$\text{toLex } d < \phi.lexOrder \Rightarrow \operatorname{coeff}(d,\phi) = 0$$$

Lean4

theorem coeff_eq_zero_of_lt_lexOrder {φ : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : toLex d < lexOrder φ) : coeff d φ = 0 :=
  by
  by_cases hφ : φ = 0
  · simp only [hφ, map_zero]
  · rcases lexOrder_def_of_ne_zero hφ with ⟨ne, hφ'⟩
    rw [hφ', WithTop.coe_lt_coe] at h
    by_contra h'
    exact WellFounded.not_lt_min _ (toLex '' φ.support) ne (Set.mem_image_equiv.mpr h') h

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