Theorems · Definition · commutative algebra
MvPowerSeries.coeff
{σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → (σ →₀ ℕ) → MvPowerSeries σ R →ₗ[R] RThe nth coefficient of a multivariate formal power series.
- Defined in
- Mathlib.RingTheory.MvPowerSeries.Basic
- Cited by
- 273 results in Mathlib
- Foundations
- Depth 28 from the axioms, rests on 239 definitions · uses propext, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- LinearMapstatement · cited by 10,215
- Finsuppstatement and proof · cited by 5,255
- MvPowerSeriesstatement · cited by 659
- LinearMap.projproof · cited by 71
Cited by296
Results whose statement or proof uses this declaration.
- PowerSeries.coeffproof · cited by 324
- MvPowerSeries.constantCoeffproof · cited by 98
- MvPowerSeries.extstatement and proof · cited by 58
- PowerSeries.coeff_zero_eq_constantCoeffproof · cited by 41
- MvPowerSeries.mapproof · cited by 34
- PowerSeries.coeff_mulproof · cited by 29
- MvPowerSeries.coeff_mulstatement · cited by 22
- MvPowerSeries.truncFinsetproof · cited by 18
- MvPowerSeries.coeff_monomialstatement · cited by 17
- MvPowerSeries.coeff_subststatement and proof · cited by 15
- MvPowerSeries.rescaleproof · cited by 14
- MvPowerSeries.coeff_eq_zero_of_lt_weightedOrderstatement and proof · cited by 14
Showing the 200 most cited of 296.