Theorems · Definition · commutative algebra
MvPowerSeries.weightedHomogeneousComponent
{σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → (σ → ℕ) → ℕ → MvPowerSeries σ R →ₗ[R] MvPowerSeries σ RThe weighted homogeneous components of an MvPowerSeries f.
- Defined in
- Mathlib.RingTheory.MvPowerSeries.Order
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 80 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.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- LinearMapstatement · cited by 10,215
- Finsuppproof · cited by 5,255
- MvPowerSeriesstatement and proof · cited by 659
- MvPowerSeries.coeffproof · cited by 273
- Finsupp.weightproof · cited by 90
Cited by8
Results whose statement or proof uses this declaration.
- MvPowerSeries.homogeneousComponentproof · cited by 13
- MvPowerSeries.coeff_weightedHomogeneousComponentstatement · cited by 5
- MvPowerSeries.isWeightedHomogeneous_weightedHomogeneousComponentstatement · cited by 3
- MvPowerSeries.weightedOrder_mulproof · cited by 2
- MvPowerSeries.weightedHomogeneousComponent_of_weightedOrderstatement and proof · cited by 2
- MvPowerSeries.weightedHomogeneousComponent_mul_of_le_weightedOrderstatement and proof · cited by 2
- MvPowerSeries.weightedHomogeneousComponent_of_lt_weightedOrder_eq_zerostatement · cited by 2
- MvPowerSeries.isWeightedHomogeneous_iff_eq_weightedHomogeneousComponentstatement and proof · cited by 1