AlgebraicCurve.Place.deg_ne_zero_of_finiteDimensional_adjoin
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_deg_ne_zero_of_finiteDimensional_adjoin
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_placeOfPointLean source · statement
theorem _root_.AlgebraicCurve.Place.deg_ne_zero_of_finiteDimensional_adjoin {K F : Type*} [Field K]
[Field F] [Algebra K F]
(x : F) (hx : Transcendental K x) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F))
F]
(v : AlgebraicCurve.Place K F) : v.deg ≠ 0