AlgebraicCurve.RationalFunctionField.degree_eq_zero_of_isPrincipal
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_degree_eq_zero_of_isPrincipal
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.degree_eq_zero_of_isPrincipal {K : Type*}
[Field K] {D : Divisor K (RatFunc K)} (hD : D.IsPrincipal) : Divisor.degree D = 0