algebraMap_fst_apply — Mathlib

English

For x ∈ K and v an infinite place of K, the first component of the image of x under the algebra map to the Adele ring is x itself.

Русский

Для x ∈ K и v бесконечного места K, первая координата образа x через отображение алгебраMap в адельное кольцо равна x.

LaTeX

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

Lean4

@[simp]
theorem algebraMap_fst_apply (x : K) (v : InfinitePlace K) : (algebraMap K (AdeleRing R K) x).1 v = x :=
  rfl

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