algebraMap_snd_apply — Mathlib

English

For x ∈ K and v ∈ HeightOneSpectrum R, the second component of the image under algebraMap to the Adele ring equals x.

Русский

Для x ∈ K и v ∈ HeightOneSpectrum R вторая координата образа через algebraMap в адельное кольцо равна x.

LaTeX

$$$$(\\mathrm{algebraMap}_K(\\mathrm{AdeleRing}(R,K))\, x)^{(2)}_v = x$$$$

Lean4

@[simp]
theorem algebraMap_snd_apply (x : K) (v : HeightOneSpectrum R) : (algebraMap K (AdeleRing R K) x).2 v = x :=
  rfl

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