ext — Mathlib

English

Two formal power series are equal iff all their coefficients agree.

Русский

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

LaTeX

$$$ \forall φ, ψ : R\langle\langle X\rangle\rangle,\,(\forall n, coeff(n)\, φ = coeff(n)\, ψ) \Rightarrow φ = ψ $$$

Lean4

/-- Two formal power series are equal if all their coefficients are equal. -/
@[ext]
theorem ext {φ ψ : R⟦X⟧} (h : ∀ n, coeff n φ = coeff n ψ) : φ = ψ :=
  MvPowerSeries.ext fun n => by
    rw [← coeff_def]
    · apply h
    rfl

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