AlgebraicCurve.Place.exists_sub_algebraMap_mem_nonunits_of_isAlgClosed
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_sub_algebraMap_mem_nonunits_of_isAlgClosed
open AlgebraicCurve
open scoped PointwiseLean source · statement
theorem _root_.AlgebraicCurve.Place.exists_sub_algebraMap_mem_nonunits_of_isAlgClosed
{κ' : Type*} [Field κ'] [IsAlgClosed κ'] {F' : Type*} [Field F'] [Algebra κ' F']
(P' : Place κ' F') [P'.FiniteResidue]
(x : F') (hx : x ∈ P'.toValuationSubring) :
∃ c : κ', x - algebraMap κ' F' c ∈ P'.toValuationSubring.nonunits