Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_truncTotal

∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPowerSeries σ R)
  {x : σ →₀ ℕ}, Finsupp.degree x < n → MvPolynomial.coeff x ((MvPowerSeries.truncTotal n) p) = (MvPowerSeries.coeff x) p

Defined in

Mathlib.RingTheory.MvPowerSeries.Trunc

Cited by

10 results in Mathlib

Foundations

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

Assumes

FiniteCommSemiring