Theorems · Definition · commutative algebra
MvPowerSeries.weightedOrder
{σ : Type u_1} → {R : Type u_2} → [Semiring R] → (σ → ℕ) → MvPowerSeries σ R → ℕ∞The weighted order with respect to w : σ → ℕ. This is the minimum value
of weight w d over all exponents d with nonzero coefficient coeff d f.
- Defined in
- Mathlib.RingTheory.MvPowerSeries.Order
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Top.topproof · cited by 9,680
- ENatstatement · cited by 4,985
- MvPowerSeriesstatement and proof · cited by 659
- Nat.findproof · cited by 139
Cited by38
Results whose statement or proof uses this declaration.
- MvPowerSeries.orderproof · cited by 45
- MvPowerSeries.coeff_eq_zero_of_lt_weightedOrderstatement and proof · cited by 14
- MvPowerSeries.le_weightedOrderstatement · cited by 7
- MvPowerSeries.le_weightedOrder_mulstatement and proof · cited by 7
- MvPowerSeries.ne_zero_iff_weightedOrder_finitestatement · cited by 5
- MvPowerSeries.exists_coeff_ne_zero_and_weightedOrderstatement and proof · cited by 4
- MvPowerSeries.weightedOrder_lestatement · cited by 4
- MvPowerSeries.nat_le_weightedOrderstatement and proof · cited by 3
- MvPowerSeries.weightedOrder_eq_top_iffstatement and proof · cited by 3
- MvPowerSeries.le_weightedOrder_prodstatement and proof · cited by 3
- MvPowerSeries.le_weightedOrder_subststatement and proof · cited by 3
- MvPowerSeries.min_weightedOrder_le_addstatement and proof · cited by 2