orderTop_add_le_mul

Mathlib.RingTheory.HahnSeries.Multiplication

URI: https://scilib.ai/kg/mathlib#HahnSeries.orderTop_add_le_mul

← MathLib Explorer

English

The combined order is at least the sum of the individual top orders.

Русский

Общий порядок не хуже суммы верхних порядков.

LaTeX

$$$ orderTop(x) + orderTop(y) \leq orderTop(x y) $$$

Lean4

theorem orderTop_add_le_mul {x y : HahnSeries Γ R} : x.orderTop + y.orderTop ≤ (x * y).orderTop :=
  by
  rw [← smul_eq_mul]
  exact HahnModule.orderTop_vAdd_le_orderTop_smul fun i j ↦ rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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