isAlgClosure_of_transcendence_basis

English

If v is a transcendence basis of K over R, then the closure Adjoin R range v is algebraic over K.

Русский

Если v — базис транскендентности K над R, то замыкание по R от Range(v) над K является алгебраически замкнутым над K.

LaTeX

$$IsAlgClosure (Algebra.adjoin R (Set.range v)) K$$

Lean4

theorem isAlgClosure_of_transcendence_basis [IsAlgClosed K] (hv : IsTranscendenceBasis R v) :
    IsAlgClosure (Algebra.adjoin R (Set.range v)) K :=
  letI := RingHom.domain_nontrivial (algebraMap R K)
  { isAlgClosed := by infer_instance
    isAlgebraic := hv.isAlgebraic }

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