orbitRelEquiv_apply_mk'' — Mathlib

English

The orbit equivalence maps the mk'' of w to the base restriction of w.

Русский

Эквивалентность орбит отображает mk'' бесконечного места в ограничение на осн. поле.

LaTeX

$$$ \text{orbitRelEquiv}(\mathrm{Quotient.mk''}(w)) = \mathrm{comap}(w)(\mathrm{algebraMap}_{kK}) $$$

Lean4

theorem orbitRelEquiv_apply_mk'' [IsGalois k K] (w : InfinitePlace K) :
    orbitRelEquiv (Quotient.mk'' w) = comap w (algebraMap k K) :=
  rfl

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