ext — Mathlib

English

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

Русский

Две многовекторные формальные степенные серии равны, если равны все их коэффициенты.

LaTeX

$$$\\phi = \\psi \\;\\text{если}\\; \\forall n, \\mathrm{coeff}(n)\\,\\phi = \\mathrm{coeff}(n)\\,\\psi$$$

Lean4

/-- Two multivariate formal power series are equal if all their coefficients are equal. -/
@[ext]
theorem ext {φ ψ : MvPowerSeries σ R} (h : ∀ n : σ →₀ ℕ, coeff n φ = coeff n ψ) : φ = ψ :=
  funext h

Похожие утверждения