map_injective — Mathlib

English

If f is injective, the induced map on power series is injective.

Русский

Если f инъективен, то отображение степенных рядов инъективно.

LaTeX

$$$\mathrm{Injective}(\mathrm{PowerSeries.map}\, f)$$$

Lean4

theorem map_injective (f : S →+* T) (hf : Function.Injective ⇑f) : Function.Injective (PowerSeries.map f) :=
  by
  intro u v huv
  ext k
  apply hf
  rw [← PowerSeries.coeff_map, ← PowerSeries.coeff_map, huv]

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