Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_coeff_finSuccEquiv

∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (p : MvPowerSeries (Fin (n + 1)) R) {k : ℕ} {x : Fin n →₀ ℕ},
  (MvPowerSeries.coeff x) ((PowerSeries.coeff k) ((MvPowerSeries.finSuccEquiv R n) p)) =
    (MvPowerSeries.coeff (Finsupp.cons k x)) p

Defined in: Mathlib.RingTheory.MvPowerSeries.Equiv
Cited by: 3 results in Mathlib
Foundations: Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
RingHom.idstatement · cited by 18,349
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement · cited by 10,215
Finsuppstatement and proof · cited by 5,255
AlgEquivstatement · cited by 1,681
PowerSeriesstatement · cited by 797
MvPowerSeriesstatement and proof · cited by 659
PowerSeries.coeffstatement and proof · cited by 324
MvPowerSeries.coeffstatement and proof · cited by 273
Equiv.toEmbeddingproof · cited by 254
Finsupp.consstatement and proof · cited by 29

Cited by3

Results whose statement or proof uses this declaration.

MvPowerSeries.finSuccEquiv_Cproof · cited by 1
MvPowerSeries.finSuccEquiv_X_zeroproof · cited by 0
MvPowerSeries.finSuccEquiv_X_succproof · cited by 0