algebraMap_surjective_of_isIntegral'

English

The surjectivity of algebraMap k K follows from the bijectivity of algebraMap k K in the integral case.

Русский

Суръективность algebraMap k K следует из биективности в случае интегральности.

LaTeX

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

Lean4

@[deprecated "ringHom_bijective_of_isIntegral" (since := "2025-04-16")]
theorem algebraMap_surjective_of_isIntegral' {k K : Type*} [Field k] [CommRing K] [IsDomain K] [IsAlgClosed k]
    (f : k →+* K) (hf : f.IsIntegral) : Function.Surjective f :=
  (ringHom_bijective_of_isIntegral f hf).surjective

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