weightedOrder_zero

Mathlib.RingTheory.MvPowerSeries.Order

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

English

The weighted order of the zero series is top (infinite).

Русский

Весовой порядок нулевого ряда равен бесконечности.

LaTeX

$$$\text{weightedOrder}(0)=\top$.$$

Lean4

@[simp]
theorem weightedOrder_zero : (0 : MvPowerSeries σ R).weightedOrder w = ⊤ := by rw [weightedOrder, dif_pos rfl]

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

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

Разделы

Аффилиация

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