order_add_of_order_ne — Mathlib

English

If the orders of f and g are different, the order of their sum is the infimum of the two orders.

Русский

Если порядки f и g различны, то порядок суммы равен infimum двух порядков.

LaTeX

$$$ f.\operatorname{order} \neq g.\operatorname{order} \Rightarrow \operatorname{ord}(f+g) = \operatorname{ord}(f) \sqcap \operatorname{ord}(g) $$$

Lean4

/-- The order of the sum of two formal power series
is the minimum of their orders if their orders differ. -/
theorem order_add_of_order_ne (h : f.order ≠ g.order) : order (f + g) = order f ⊓ order g :=
  weightedOrder_add_of_weightedOrder_ne _ h

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