AlgebraicCurve.Place.mem_range_algebraMap_of_forall_ord_eq_zero
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_range_algebraMap_of_forall_ord_eq_zero
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 IntermediateField.algebraAdjoinAdjoinLean source · statement
theorem _root_.AlgebraicCurve.Place.mem_range_algebraMap_of_forall_ord_eq_zero {K F : Type*} [Field
K] [CharZero K] [Field F] [Algebra K F] [IsAlgClosed K] (j : F) (hj : Transcendental K j)
[FiniteDimensional (IntermediateField.adjoin K ({j} : Set F)) F] {x : F} (hx : ∀ v : Place K F,
v.ord x = 0) : x ∈ (algebraMap K F).range