Theorems · Theorem · commutative algebra

MvPowerSeries.min_weightedOrder_le_add

∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
  min (MvPowerSeries.weightedOrder w f) (MvPowerSeries.weightedOrder w g) ≤ MvPowerSeries.weightedOrder w (f + g)

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

Defined in

Mathlib.RingTheory.MvPowerSeries.Order

Cited by

2 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring