comap_mk — Mathlib

English

Let φ be a ring hom K → ℂ and f be a ring hom k → K. Then the infinite place on k obtained by pulling back φ along f equals the infinite place associated to φ ∘ f on k.

Русский

Пусть φ: K → ℂ и f: k → K – гомоморфизмы колец. Тогда бесконечное место на k, полученное как обратное по f, совпадает с бесконечным местом, соответствующим φ ∘ f на k.

LaTeX

$$$ (\mathrm{mk}(\phi)).\mathrm{comap} f = \mathrm{mk}(\phi \circ f) $$$

Lean4

@[simp]
theorem comap_mk (φ : K →+* ℂ) (f : k →+* K) : (mk φ).comap f = mk (φ.comp f) :=
  rfl

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