comap_mk_lift — Mathlib

English

If two infinite places w and v on k correspond under a comap with f, their values agree after composing with f.

Русский

Если два бесконечных места совпадают после обратной по f, их значения согласуются после композиции с f.

LaTeX

$$$ w.\mathrm{comap} f = v \Rightarrow \forall x, w(f(x)) = v(x) $$$

Lean4

theorem comap_mk_lift [Algebra k K] [Algebra.IsAlgebraic k K] (φ : k →+* ℂ) :
    (mk (ComplexEmbedding.lift K φ)).comap (algebraMap k K) = mk φ := by simp

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