Theorems · Theorem · commutative algebra

MvPowerSeries.constantCoeff_expand

∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R),
  MvPowerSeries.constantCoeff ((MvPowerSeries.expand p hp) φ) = MvPowerSeries.constantCoeff φ

Defined in

Mathlib.RingTheory.MvPowerSeries.Expand

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing