lexOrder_le_of_coeff_ne_zero — Mathlib

English

The same leading coefficient fact as in 181243, with simp lemmas; the leading coefficient is nonzero.

Русский

То же утверждение о ведущем коэффициенте, используя упрощённые леммы; ведущий коэффициент ненулевой.

LaTeX

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

Lean4

theorem lexOrder_le_of_coeff_ne_zero {φ : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : coeff d φ ≠ 0) : lexOrder φ ≤ toLex d :=
  by
  rw [← not_lt]
  intro h'
  exact h (coeff_eq_zero_of_lt_lexOrder h')

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