AlgebraicCurve.nonempty_place_of_transcendental_of_finiteDimensional
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Nonempty_place_of_transcendental_of_finiteDimensional
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdealLean source · statement
theorem _root_.AlgebraicCurve.nonempty_place_of_transcendental_of_finiteDimensional
(k : Type*) [Field k] {F : Type*} [Field F] [Algebra k F] (x : F) (hx : Transcendental k x)
(hfin : FiniteDimensional ↥(IntermediateField.adjoin k ({x} : Set F)) F)
[Algebra.IsSeparable ↥(IntermediateField.adjoin k ({x} : Set F)) F] :
Nonempty (AlgebraicCurve.Place k F)