AlgebraicCurve.RationalFunctionField.ord_ofHeightOneSpectrum_eq_neg_log
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_ord_ofHeightOneSpectrum_eq_neg_log
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 IsDedekindDomain WithZero IsLocalRing
open scoped PolynomialLean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.ord_ofHeightOneSpectrum_eq_neg_log {K :
Type*} [Field K] (w : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) {p : Polynomial K}
(hp : p ≠ 0) (hw : w.asIdeal = Ideal.span {p}) {f : RatFunc K} (hf : f ≠ 0) :
(Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).ord f = -WithZero.log (w.valuation
(RatFunc K) f)