equivInfinitePlace_apply — Mathlib

English

The conjugation/real restriction equivInfinitePlace K applied to a place w is simply the restriction of w via comap with the real subfield.

Русский

Применение эквивалента бесконечных мест к месту w есть ограничение w на K⁺ через comap.

LaTeX

$$$\\text{equivInfinitePlace }K\\, w = w^{\\text{comap}}(\\text{algebraMap } K^+ \\to K).$$$

Lean4

@[simp]
theorem equivInfinitePlace_apply (w : InfinitePlace K) : equivInfinitePlace K w = w.comap (algebraMap K⁺ K) :=
  rfl

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