Theorems · Theorem · commutative algebra

PowerSeries.ext

∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R},
  (∀ (n : ℕ), (PowerSeries.coeff n) φ = (PowerSeries.coeff n) ψ) → φ = ψ

Two formal power series are equal if all their coefficients are equal.

Defined in

Mathlib.RingTheory.PowerSeries.Basic

Cited by

69 results in Mathlib

Foundations

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

Assumes

Semiring