Theorems · Definition · commutative algebra

MvPowerSeries.truncTotal

{σ : Type u_1} → [Finite σ] → {R : Type u_4} → [inst : CommSemiring R] → ℕ → MvPowerSeries σ R →ₗ[R] MvPolynomial σ R

The truncation of a multivariate formal power series at a total degree n when the index σ is finite.

Defined in

Mathlib.RingTheory.MvPowerSeries.Trunc

Cited by

28 results in Mathlib

Foundations

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

Assumes

FiniteCommSemiring