AlgebraicCurve.Place.exists_ord_neg_of_transcendental
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_ord_neg_of_transcendental
attribute [-instance]
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve
open scoped nonZeroDivisorsLean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_neg_of_transcendental {K F : Type*} [Field K]
[CharZero K] [Field F] [Algebra K F] (x : F) (hx : Transcendental K x) [FiniteDimensional
(IntermediateField.adjoin K ({x} : Set F)) F] : ∃ v : Place K F, v.ord x < 0