equivInfinitePlace_symm_apply — Mathlib

English

The inverse of the infinite place equivalence sends the place in K⁺ back to K by the corresponding algebra maps.

Русский

Обратное к эквивалентности бесконечных мест восстанавливает место в K через соответствующую алгебраическую карту.

LaTeX

$$$(equivInfinitePlace K)^{-1} (w) (\\text{via } \\mathcal{O}_K \\to K) = w$.$$

Lean4

@[simp]
theorem equivInfinitePlace_symm_apply (w : InfinitePlace K⁺) (x : K⁺) :
    (equivInfinitePlace K).symm w (algebraMap K⁺ K x) = w x := by
  rw [← comap_apply, ← equivInfinitePlace_apply, Equiv.apply_symm_apply]

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