exists_finsupp_eq_lexOrder_of_ne_zero

English

For a nonzero φ, there exists a finite exponent vector d such that φ.lexOrder equals toLex d.

Русский

Для ненулевого φ существует вектор показателей d, такой что φ.lexOrder равен toLex d.

LaTeX

$$$φ \neq 0 \Rightarrow \exists d : σ \to_0 \mathbb{N},\; φ.\text{lexOrder} = toLex d$$$

Lean4

theorem exists_finsupp_eq_lexOrder_of_ne_zero {φ : MvPowerSeries σ R} (hφ : φ ≠ 0) :
    ∃ (d : σ →₀ ℕ), lexOrder φ = toLex d :=
  by
  simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, WithTop.ne_top_iff_exists] at hφ
  obtain ⟨p, hp⟩ := hφ
  exact ⟨ofLex p, by simp only [toLex_ofLex, hp]⟩

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