ringHom_bijective_of_isIntegral — Mathlib

English

If f : k →+* K is integral, then f is bijective.

Русский

Если отображение кольца f : k →+* K интегрально, то оно биективно.

LaTeX

$$$\forall {k K} [\mathrm{Field}\;k] [\mathrm{CommRing}\;K] [\mathrm{IsDomain}\;K] [IsAlgClosed k] (f : k \to+* K) (hf : f.IsIntegral), \; Function.Bijective f$$$

Lean4

theorem ringHom_bijective_of_isIntegral {k K : Type*} [Field k] [CommRing K] [IsDomain K] [IsAlgClosed k] (f : k →+* K)
    (hf : f.IsIntegral) : Function.Bijective f :=
  let _ : Algebra k K := f.toAlgebra
  have : Algebra.IsIntegral k K := ⟨hf⟩
  algebraMap_bijective_of_isIntegral

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