order_mul

Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

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

English

The order of the product of two mv-power-series equals the sum of their orders: (f*g).order = f.order + g.order.

Русский

Порядок произведения mv-рядов равен сумме их порядков.

LaTeX

$$$ (f*g).order = f.order + g.order $.$$

Lean4

theorem order_mul (f g : MvPowerSeries σ R) : (f * g).order = f.order + g.order :=
  weightedOrder_mul _ f g

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

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

Разделы

Аффилиация

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