order

Mathlib.RingTheory.MvPowerSeries.Order

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.order

English

The order of a mv_power_series is defined as the weighted order with weight function identically 1.

Русский

Порядок mv_power_series определяется как взвешенный порядок при весовой функции, равной единице.

LaTeX

$$order f := weightedOrder (fun _ => 1) f$$

Lean4

/-- The order of a mv_power_series -/
def order (f : MvPowerSeries σ R) : ℕ∞ :=
  weightedOrder (fun _ => 1) f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru