weightedOrder — Mathlib

English

The weighted order of a mvPowerSeries is defined as an ENat value depending on the weight function w; if f=0 then it is ∞, otherwise it is the least weight where a coefficient is nonzero.

Русский

Взвешенный порядок mv-рядов — это ENat-значение, равное ∞ для нулевого ряда, иначе минимальный вес, при котором соответствующий коэффициент не равен нулю.

LaTeX

$$$\text{weightedOrder}(f)=\begin{cases} \top,& f=0, \\ \text{Nat.find }(\ldots ),& f\neq 0.\end{cases}$$$

Lean4

/-- The weighted order of a mv_power_series -/
def weightedOrder (f : MvPowerSeries σ R) : ℕ∞ := by
  classical exact dite (f = 0) (fun _ => ⊤) fun h => Nat.find ((ne_zero_iff_exists_coeff_ne_zero_and_weight w).mp h)

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