rescale_injective — Mathlib

English

For any nonzero a in R, the rescale map by a is injective on power series.

Русский

Для любого ненулевого a ∈ R отображение рескейла по a инъективно на степенных рядах.

LaTeX

$$For a ≠ 0, Function.Injective( PowerSeries.rescale(a) )$$

Lean4

theorem rescale_injective {a : R} (ha : a ≠ 0) : Function.Injective (rescale a) :=
  by
  intro p q h
  rw [PowerSeries.ext_iff] at *
  intro n
  specialize h n
  rwa [coeff_rescale, coeff_rescale, mul_right_inj' <| pow_ne_zero _ ha] at h

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