C_injective — Mathlib

English

The map C: R → HahnSeries Γ R is injective; distinct coefficients give distinct Hahn series.

Русский

Отображение C: R → HahnSeries Γ R инъективно; различные коэффициенты дают различные Hahn-серии.

LaTeX

$$$ \forall r,s\in R,\ C(r)=C(s)\Rightarrow r=s $$$

Lean4

theorem C_injective : Function.Injective (C : R → HahnSeries Γ R) :=
  by
  intro r s rs
  rw [HahnSeries.ext_iff, funext_iff] at rs
  have h := rs 0
  rwa [C_apply, coeff_single_same, C_apply, coeff_single_same] at h

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