algebraMap_injective — Mathlib

English

Assuming K is a number field, the map algebraMap_K: K → AdeleRing(R,K) is injective.

Русский

При условии, что K — число поле, отображение algebraMap_K: K → AdeleRing(R,K) инъективно.

LaTeX

$$$$ \\operatorname{Injective}(\\mathrm{algebraMap}_K(\\mathrm{AdeleRing}(R,K))) $$$$

Lean4

theorem algebraMap_injective [NumberField K] : Function.Injective (algebraMap K (AdeleRing R K)) := fun _ _ hxy =>
  (algebraMap K _).injective (Prod.ext_iff.1 hxy).1

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