Theorems · Theorem · field theory

IsAlgClosed.of_denseRange

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : NontriviallyNormedField L] [CompleteSpace L] [CharZero L]
  [IsUltrametricDist L] [inst_5 : Algebra K L], DenseRange ⇑(algebraMap K L) → ∀ [IsAlgClosed K], IsAlgClosed L

If K is an algebraically closed dense subfield of a complete nonarchimedean normed field L of characteristic zero, then L is also algebraically closed.

Defined in

Mathlib.Analysis.Normed.Field.Dense

Cited by

0 results in Mathlib

Foundations

Depth 241 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNontriviallyNormedFieldCompleteSpaceCharZeroIsUltrametricDistAlgebraIsAlgClosed