coe_injective — Mathlib

English

The map φ ↦ φ.toPowerSeries from polynomials to power series is injective: it never collapses two distinct polynomials.

Русский

Отображение φ ↦ φ.toPowerSeries из полиномов в ряд степенных является инъективным.

LaTeX

$$$\\forall \\varphi,\\psi\\,\\, (\\varphi : PowerSeries R) = (\\psi) \\Rightarrow \\varphi = \\psi$$$

Lean4

theorem coe_injective : Function.Injective ((↑) : R[X] → PowerSeries R) := fun x y h =>
  by
  ext
  simp_rw [← coeff_coe, h]

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