Theorems · Theorem · commutative algebra

MvPowerSeries.ext_iff

∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ ψ : MvPowerSeries σ R},
  φ = ψ ↔ ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) φ = (MvPowerSeries.coeff n) ψ

Two multivariate formal power series are equal if and only if all their coefficients are equal.

Defined in

Mathlib.RingTheory.MvPowerSeries.Basic

Cited by

5 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound

Assumes

Semiring