le_order_mul — Mathlib

English

The order of the product of two power series is at least the sum of their orders.

Русский

Порядок произведения двух рядов не меньше суммы их порядков.

LaTeX

$$$ \operatorname{ord}(f) + \operatorname{ord}(g) \le \operatorname{ord}(f g) $$$

Lean4

/-- The order of the product of two formal power series
is at least the sum of their orders. -/
theorem le_order_mul : f.order + g.order ≤ order (f * g) :=
  le_weightedOrder_mul _

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