English
For any r ∈ k, (C(σ) r)⁻¹ = C r⁻¹; in particular, when r ≠ 0 this holds; if r = 0, the convention gives equality with 0.
Русский
Для любого r ∈ k, (C(σ) r)⁻¹ = C r⁻¹; особенно, если r ≠ 0 это верно; если r = 0, равенство следует из соглашения 0⁻¹ = 0.
LaTeX
$$$ (C(\sigma:=\sigma)\; r)^{-1} = C\; r^{-1} $$$
Lean4
theorem le_lexOrder_iff {φ : MvPowerSeries σ R} {w : WithTop (Lex (σ →₀ ℕ))} :
w ≤ lexOrder φ ↔ (∀ (d : σ →₀ ℕ) (_ : toLex d < w), coeff d φ = 0) :=
by
constructor
· intro h d hd
apply coeff_eq_zero_of_lt_lexOrder
exact lt_of_lt_of_le hd h
· intro h
rw [← not_lt]
intro h'
have hφ : φ ≠ 0 := by
rw [ne_eq, ← lexOrder_eq_top_iff_eq_zero]
exact ne_top_of_lt h'
obtain ⟨d, hd⟩ := exists_finsupp_eq_lexOrder_of_ne_zero hφ
refine coeff_ne_zero_of_lexOrder hd.symm (h d ?_)
rwa [← hd]
