Module

RationalFunctionField_hasPrincipalDivisors.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_hasPrincipalDivisors

1 declaration indexed from sourceView source ↗

Module documentation

RationalFunctionField hasPrincipalDivisors

A rational function field has principal divisors with finite support and degree zero.

Imports4

Imported by13

theorem

hasPrincipalDivisors

L40 ↗

AlgebraicCurve.RationalFunctionField.hasPrincipalDivisors

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_hasPrincipalDivisors
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 Polynomial

Lean source · statement

theorem _root_.AlgebraicCurve.RationalFunctionField.hasPrincipalDivisors (K : Type*) [Field K] :
  HasPrincipalDivisors K (RatFunc K)

Module documentation

RationalFunctionField hasPrincipalDivisors

Declarations

hasPrincipalDivisors