NYLL
Module

RationalFunctionField_isPrincipal_of_degree_eq_zero.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_isPrincipal_of_degree_eq_zero
15 declarations indexed from sourceView source ↗

Module documentation

Rational Function Field is Principal of degree eq zero

Imports10
Imported by2

Declarations

theorem

ord_prod

L56 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.ord_prod
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
theorem ord_prod {F : Type*} [Field F] [Algebra K F] (v : Place K F) {ι : Type*} (s : Finset ι)
    (g : ι → F) (hg : ∀ i ∈ s, g i ≠ 0) :
    v.ord (∏ i ∈ s, g i) = ∑ i ∈ s, v.ord (g i)
abbrev

IsFinite

L70 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.IsFinite
Documentation

The condition that a rational-function place comes from a height-one prime of the polynomial ring.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
abbrev IsFinite (v : Place K (RatFunc K)) : Prop
def

spec

L74 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.spec
Documentation

A height-one prime representing the given finite rational-function place.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
def spec {v : Place K (RatFunc K)} (hv : IsFinite v) : HeightOneSpectrum K[X]
theorem

eq_ofHeightOneSpectrum_spec

L76 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.eq_ofHeightOneSpectrum_spec
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
theorem eq_ofHeightOneSpectrum_spec {v : Place K (RatFunc K)} (hv : IsFinite v) :
    v = Place.ofHeightOneSpectrum (spec hv)
def

gen

L81 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.gen
Documentation

A generator of the prime of a finite place, with polynomial one assigned at infinity.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
open Classical in
Lean source · statement
def gen (v : Place K (RatFunc K)) : K[X]
theorem

span_gen

L84 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.span_gen
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
theorem span_gen {v : Place K (RatFunc K)} (hv : IsFinite v) :
    (spec hv).asIdeal = Ideal.span {gen v}
theorem

gen_of_not_isFinite

L89 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.gen_of_not_isFinite
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
theorem gen_of_not_isFinite {v : Place K (RatFunc K)} (hv : ¬ IsFinite v) : gen v = 1
theorem

gen_ne_zero

L92 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.gen_ne_zero
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
theorem gen_ne_zero (v : Place K (RatFunc K)) : gen v ≠ 0
theorem

algebraMap_gen_ne_zero

L98 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.algebraMap_gen_ne_zero
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
theorem algebraMap_gen_ne_zero (v : Place K (RatFunc K)) :
    algebraMap K[X] (RatFunc K) (gen v) ≠ 0
theorem

ord_gen_of_isFinite

L103 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.ord_gen_of_isFinite
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
open Classical in
Lean source · full declaration
theorem ord_gen_of_isFinite {u : Place K (RatFunc K)} (hu : IsFinite u) (v : Place K (RatFunc K)) :
    u.ord (algebraMap K[X] (RatFunc K) (gen v)) = if v = u then 1 else 0 := by
  classical
  by_cases hvu : v = u
  · subst hvu
    rw [ite_eq_left rfl]
    have h := ord_ofHeightOneSpectrum_of_span (spec hu) (gen_ne_zero v) (span_gen hu)
    rwa [← eq_ofHeightOneSpectrum_spec hu] at h
  rw [ite_eq_right hvu]
  by_cases hv : IsFinite v
  · by_contra hne
    rw [eq_ofHeightOneSpectrum_spec hu] at hne
    have hmem : gen v ∈ (spec hu).asIdeal :=
      (Place.ord_ofHeightOneSpectrum_ne_zero_iff (K := K) (F := RatFunc K) (spec hu)
        (gen_ne_zero v)).mp hne
    have hle : (spec hv).asIdeal ≤ (spec hu).asIdeal := by
      rw [span_gen hv, Ideal.span_singleton_le_iff_mem]
      exact hmem
    have heq : (spec hv).asIdeal = (spec hu).asIdeal :=
      (spec hv).isMaximal.eq_of_le (spec hu).isPrime.ne_top hle
    exact hvu (by rw [eq_ofHeightOneSpectrum_spec hv, eq_ofHeightOneSpectrum_spec hu,
      HeightOneSpectrum.ext heq])
  · rw [gen_of_not_isFinite hv, map_one, Place.ord_one]
theorem

ord_gen_of_not_isFinite

L128 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.ord_gen_of_not_isFinite
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
open Classical in
Lean source · full declaration
theorem ord_gen_of_not_isFinite {u : Place K (RatFunc K)} (hu : ¬ IsFinite u)
    (v : Place K (RatFunc K)) :
    u.ord (algebraMap K[X] (RatFunc K) (gen v)) = -(v.deg : ℤ) + if v = u then 1 else 0 := by
  classical
  have hu' : ∀ w : HeightOneSpectrum K[X], u ≠ Place.ofHeightOneSpectrum w :=
    fun w h => hu ⟨w, h⟩
  by_cases hv : IsFinite v
  · have hvu : v ≠ u := fun h => hu (h ▸ hv)
    rw [ite_eq_right hvu, add_zero,
      ord_eq_neg_intDegree_of_forall_ne_ofHeightOneSpectrum u hu' (algebraMap_gen_ne_zero v),
      RatFunc.intDegree_polynomial]
    conv_rhs => rw [eq_ofHeightOneSpectrum_spec hv, deg_ofHeightOneSpectrum K (span_gen hv)]
  · have hv' : ∀ w : HeightOneSpectrum K[X], v ≠ Place.ofHeightOneSpectrum w :=
      fun w h => hv ⟨w, h⟩
    have hvu : v = u := subsingleton_setOf_forall_ne_ofHeightOneSpectrum hv' hu'
    rw [ite_eq_left hvu, gen_of_not_isFinite hv, map_one, Place.ord_one,
      deg_eq_one_of_forall_ne_ofHeightOneSpectrum v hv']
    norm_num
def

genFactor

L149 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.genFactor
Documentation

The rational-function factor obtained by raising the place generator to its divisor coefficient.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
def genFactor (D : Divisor K (RatFunc K)) (v : Place K (RatFunc K)) : RatFunc K
theorem

genFactor_ne_zero

L152 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.genFactor_ne_zero
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
theorem genFactor_ne_zero (D : Divisor K (RatFunc K)) (v : Place K (RatFunc K)) :
    genFactor D v ≠ 0
theorem

isPrincipal_of_degree_eq_zero'

L156 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_eq_zero.AlgebraicCurve.RationalFunctionField.W2B.isPrincipal_of_degree_eq_zero'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
namespace W2B
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve
variable {K : Type*} [Field K]
Lean source · statement
theorem isPrincipal_of_degree_eq_zero' (D : Divisor K (RatFunc K)) (hD : Divisor.degree D = 0) :
    D.IsPrincipal
theorem

isPrincipal_of_degree_eq_zero

L197 ↗
AlgebraicCurve.RationalFunctionField.isPrincipal_of_degree_eq_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_isPrincipal_of_degree_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 _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
open _root_.AlgebraicCurve AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.isPrincipal_of_degree_eq_zero {K : Type*}
  [Field K] (D : Divisor K (RatFunc K)) (hD : Divisor.degree D = 0) : D.IsPrincipal

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.