ker_algebraMap_eq_bot — Mathlib

English

The kernel of the algebraMap between 𝓞_K and 𝓞_L is {0}.

Русский

Ядро алгебраMap между 𝓞_K и 𝓞_L равно {0}.

LaTeX

$$$\\operatorname{ker}(\\mathrm{algebraMap}(\\mathcal{O}_K, \\mathcal{O}_L)) = \\{0\\}$$$

Lean4

/-- The kernel of the algebraMap between ring of integers is `⊥`. -/
theorem ker_algebraMap_eq_bot : RingHom.ker (algebraMap (𝓞 K) (𝓞 L)) = ⊥ :=
  (RingHom.ker_eq_bot_iff_eq_zero (algebraMap (𝓞 K) (𝓞 L))).mpr <| fun x hx =>
    by
    have h : (algebraMap K L) x = (algebraMap (𝓞 K) (𝓞 L)) x := rfl
    simp only [hx, map_zero, map_eq_zero, RingOfIntegers.coe_eq_zero_iff] at h
    exact h

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