NYLL
Module

ConstantExtension.lean

Nyll.AlgebraicCurves.Divisors.ConstantExtension
29 declarations indexed from sourceView source ↗

Module documentation

Constant Extension

Imports5
  • Mathlib.Data.Int.ConditionallyCompleteOrder
  • Mathlib.RingTheory.Henselian
  • Mathlib.RingTheory.RegularLocalRing.Defs
  • Mathlib.RingTheory.SimpleRing.Principal
  • Nyll.AlgebraicCurves.Divisors.Maps
Imported by18

Declarations

def

forgetConstants

L35 ↗
AlgebraicCurve.Place.forgetConstants
Documentation

View a place over the larger constant field as a place over the smaller constant field.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section Forget
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
Lean source · full declaration
def forgetConstants (w : Place K' F') : Place K F' where
  toValuationSubring := w.toValuationSubring
  algebraMap_mem' a := by
    rw [IsScalarTower.algebraMap_apply K K' F']
    exact w.algebraMap_mem' (algebraMap K K' a)
  ne_top' := w.ne_top'
  isPrincipalIdealRing' := w.isPrincipalIdealRing'
theorem

forgetConstants_toValuationSubring

L43 ↗
AlgebraicCurve.Place.forgetConstants_toValuationSubring
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section Forget
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
Lean source · statement
theorem forgetConstants_toValuationSubring (w : Place K' F') :
    (forgetConstants (K := K) w).toValuationSubring = w.toValuationSubring
theorem

forgetConstants_injective

L47 ↗
AlgebraicCurve.Place.forgetConstants_injective
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section Forget
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
Lean source · statement
theorem forgetConstants_injective :
    Function.Injective (forgetConstants (K := K) (K' := K') (F' := F'))
theorem

ord_forgetConstants

L52 ↗
AlgebraicCurve.Place.ord_forgetConstants
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section Forget
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
Lean source · statement
theorem ord_forgetConstants (w : Place K' F') (f : F') :
    (forgetConstants (K := K) w).ord f = w.ord f
theorem

algebraMap_mem_of_isIntegral

L68 ↗
AlgebraicCurve.Place.algebraMap_mem_of_isIntegral
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section Extend
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
variable (K') in
Lean source · statement
theorem algebraMap_mem_of_isIntegral [Algebra.IsIntegral K K'] (v : Place K F') (a : K') :
    algebraMap K' F' a ∈ v.toValuationSubring
def

extendConstants

L79 ↗
AlgebraicCurve.Place.extendConstants
Documentation

Extend the constant field of a place along an integral extension.

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
section Extend
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
variable (K') in
variable (K') in
Lean source · full declaration
def extendConstants [Algebra.IsIntegral K K'] (v : Place K F') : Place K' F' where
  toValuationSubring := v.toValuationSubring
  algebraMap_mem' := v.algebraMap_mem_of_isIntegral K'
  ne_top' := v.ne_top'
  isPrincipalIdealRing' := v.isPrincipalIdealRing'
theorem

extendConstants_toValuationSubring

L85 ↗
AlgebraicCurve.Place.extendConstants_toValuationSubring
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
section Extend
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
variable (K') in
variable (K') in
Lean source · statement
theorem extendConstants_toValuationSubring [Algebra.IsIntegral K K'] (v : Place K F') :
    (extendConstants K' v).toValuationSubring = v.toValuationSubring
def

constantFieldEquiv

L91 ↗
AlgebraicCurve.Place.constantFieldEquiv
Documentation

The equivalence of places under an integral extension of the constant field.

Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Extend
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
variable (K') in
variable (K') in
variable (K K') in
Lean source · full declaration
def constantFieldEquiv [Algebra.IsIntegral K K'] : Place K F' ≃ Place K' F' where
  toFun := extendConstants K'
  invFun := forgetConstants
  left_inv _ := Place.ext rfl
  right_inv _ := Place.ext rfl
theorem

constantFieldEquiv_apply_toValuationSubring

L97 ↗
AlgebraicCurve.Place.constantFieldEquiv_apply_toValuationSubring
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Extend
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
variable (K') in
variable (K') in
variable (K K') in
Lean source · statement
theorem constantFieldEquiv_apply_toValuationSubring [Algebra.IsIntegral K K']
    (v : Place K F') :
    (constantFieldEquiv K K' v).toValuationSubring = v.toValuationSubring
theorem

constantFieldEquiv_symm_apply

L102 ↗
AlgebraicCurve.Place.constantFieldEquiv_symm_apply
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Extend
variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
namespace Place
variable (K') in
variable (K') in
variable (K K') in
Lean source · statement
theorem constantFieldEquiv_symm_apply [Algebra.IsIntegral K K'] (w : Place K' F') :
    (constantFieldEquiv K K' (F' := F')).symm w = forgetConstants w
def

restrictConstants

L121 ↗
AlgebraicCurve.Place.restrictConstants
Documentation

Restrict a place to the smaller function field and constant field.

Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (F) in
Lean source · statement
def restrictConstants (w : Place K' F') : Place K F
theorem

restrictConstants_toValuationSubring

L124 ↗
AlgebraicCurve.Place.restrictConstants_toValuationSubring
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (F) in
Lean source · statement
theorem restrictConstants_toValuationSubring (w : Place K' F') :
    (restrictConstants F (K := K) w).toValuationSubring
      = w.toValuationSubring.comap (algebraMap F F')
theorem

ord_restrictConstants

L129 ↗
AlgebraicCurve.Place.ord_restrictConstants
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (F) in
Lean source · statement
theorem ord_restrictConstants (w : Place K' F') (f : F) :
    w.ord (algebraMap F F' f)
      = ramificationIndex (F := F) (forgetConstants (K := K) w)
          * (restrictConstants F (K := K) w).ord f
theorem

restrictConstants_fiber_finite

L136 ↗
AlgebraicCurve.Place.restrictConstants_fiber_finite
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (F) in
variable (K') in
Lean source · statement
theorem restrictConstants_fiber_finite [HasPrincipalDivisors K' F'] (v : Place K F) :
    {w : Place K' F' | restrictConstants F (K := K) w = v}.Finite
def

fiberConstants

L157 ↗
AlgebraicCurve.Place.fiberConstants
Documentation

The finite set of places lying over a place after constant-field extension.

Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (F) in
variable (K') in
variable (K' F') in
Lean source · statement
def fiberConstants [HasPrincipalDivisors K' F'] (v : Place K F) : Finset (Place K' F')
theorem

mem_fiberConstants

L160 ↗
AlgebraicCurve.Place.mem_fiberConstants
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (F) in
variable (K') in
variable (K' F') in
Lean source · statement
theorem mem_fiberConstants [HasPrincipalDivisors K' F'] {v : Place K F} {w : Place K' F'} :
    w ∈ fiberConstants K' F' v ↔ restrictConstants F (K := K) w = v
def

pullbackConstantsSingleHom

L172 ↗
AlgebraicCurve.Divisor.pullbackConstantsSingleHom
Documentation

Pull back a multiple of a single place using ramification indices in its fiber.

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Divisor
variable [HasPrincipalDivisors K' F']
variable (K' F') in
Lean source · full declaration
def pullbackConstantsSingleHom (v : Place K F) : ℤ →+ Divisor K' F' where
  toFun n := ∑ w ∈ Place.fiberConstants K' F' v,
    Finsupp.single w (n * (Place.forgetConstants (K := K) w).ramificationIndex F)
  map_zero' := by simp
  map_add' m n := by
    rw [← Finset.sum_add_distrib]
    exact Finset.sum_congr rfl fun w _ => by rw [add_mul, Finsupp.single_add]
def

pullbackConstants

L182 ↗
AlgebraicCurve.Divisor.pullbackConstants
Documentation

The additive pullback of divisors under constant-field extension.

Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Divisor
variable [HasPrincipalDivisors K' F']
variable (K' F') in
variable (K' F') in
Lean source · statement
def pullbackConstants : Divisor K F →+ Divisor K' F'
theorem

pullbackConstants_single

L185 ↗
AlgebraicCurve.Divisor.pullbackConstants_single
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Divisor
variable [HasPrincipalDivisors K' F']
variable (K' F') in
variable (K' F') in
Lean source · statement
theorem pullbackConstants_single (v : Place K F) (n : ℤ) :
    pullbackConstants K' F' (Finsupp.single v n)
      = ∑ w ∈ Place.fiberConstants K' F' v,
          Finsupp.single w (n * (Place.forgetConstants (K := K) w).ramificationIndex F)
theorem

pullbackConstants_single_apply_of_restrict_eq

L191 ↗
AlgebraicCurve.Divisor.pullbackConstants_single_apply_of_restrict_eq
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Divisor
variable [HasPrincipalDivisors K' F']
variable (K' F') in
variable (K' F') in
Lean source · statement
theorem pullbackConstants_single_apply_of_restrict_eq {v : Place K F} {w : Place K' F'}
    (hw : Place.restrictConstants F (K := K) w = v) (n : ℤ) :
    pullbackConstants K' F' (Finsupp.single v n) w
      = n * (Place.forgetConstants (K := K) w).ramificationIndex F
theorem

pullbackConstants_single_apply_of_restrict_ne

L201 ↗
AlgebraicCurve.Divisor.pullbackConstants_single_apply_of_restrict_ne
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Divisor
variable [HasPrincipalDivisors K' F']
variable (K' F') in
variable (K' F') in
Lean source · statement
theorem pullbackConstants_single_apply_of_restrict_ne {v : Place K F} {w : Place K' F'}
    (hw : Place.restrictConstants F (K := K) w ≠ v) (n : ℤ) :
    pullbackConstants K' F' (Finsupp.single v n) w = 0
theorem

pullbackConstants_apply

L209 ↗
AlgebraicCurve.Divisor.pullbackConstants_apply
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Divisor
variable [HasPrincipalDivisors K' F']
variable (K' F') in
variable (K' F') in
Lean source · statement
theorem pullbackConstants_apply (D : Divisor K F) (w : Place K' F') :
    pullbackConstants K' F' D w
      = (Place.forgetConstants (K := K) w).ramificationIndex F
          * D (Place.restrictConstants F (K := K) w)
theorem

pullbackConstants_apply_eq_ord

L224 ↗
AlgebraicCurve.Divisor.pullbackConstants_apply_eq_ord
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Divisor
variable [HasPrincipalDivisors K' F']
variable (K' F') in
variable (K' F') in
Lean source · statement
theorem pullbackConstants_apply_eq_ord {f : F} {D : Divisor K F}
    (hD : ∀ v : Place K F, D v = v.ord f) (w : Place K' F') :
    pullbackConstants K' F' D w = w.ord (algebraMap F F' f)
theorem

isPrincipal_pullbackConstants

L229 ↗
AlgebraicCurve.Divisor.isPrincipal_pullbackConstants
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Divisor
variable [HasPrincipalDivisors K' F']
variable (K' F') in
variable (K' F') in
Lean source · statement
theorem isPrincipal_pullbackConstants {D : Divisor K F} (hD : D.IsPrincipal) :
    (pullbackConstants K' F' D).IsPrincipal
theorem

pullbackConstants_mem_principal

L236 ↗
AlgebraicCurve.Divisor.pullbackConstants_mem_principal
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section Pullback
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Divisor
variable [HasPrincipalDivisors K' F']
variable (K' F') in
variable (K' F') in
Lean source · statement
theorem pullbackConstants_mem_principal {D : Divisor K F}
    (hD : D ∈ principal (K := K) (F := F)) :
    pullbackConstants K' F' D ∈ principal (K := K') (F := F')
def

baseChange

L254 ↗
AlgebraicCurve.Pic.baseChange
Documentation

The map on divisor classes induced by constant-field extension.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section ClassGroup
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']
variable (K K' F F') in
Lean source · statement
def Pic.baseChange : Pic K F →+ Pic K' F'
theorem

baseChange_mk

L258 ↗
AlgebraicCurve.Pic.baseChange_mk
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section ClassGroup
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']
variable (K K' F F') in
Lean source · statement
theorem Pic.baseChange_mk (D : Divisor K F) :
    Pic.baseChange K K' F F' (QuotientAddGroup.mk D)
      = QuotientAddGroup.mk (Divisor.pullbackConstants K' F' D)
class

ConstantFieldDegreeFormula

L265 ↗
AlgebraicCurve.ConstantFieldDegreeFormula
Documentation

The assertion that divisor degree is preserved by constant-field pullback.

Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section ClassGroup
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']
variable (K K' F F') in
variable (K K' F F') in
Lean source · full declaration
class ConstantFieldDegreeFormula : Prop where
  /-- Pullback along the constant-field extension preserves divisor degree. -/
  degree_pullbackConstants : ∀ D : Divisor K F,
    Divisor.degree (Divisor.pullbackConstants K' F' D) = Divisor.degree D
theorem

pullbackConstants_mem_degZero

L270 ↗
AlgebraicCurve.Divisor.pullbackConstants_mem_degZero
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section ClassGroup
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']
variable (K K' F F') in
variable (K K' F F') in
Lean source · statement
theorem Divisor.pullbackConstants_mem_degZero [ConstantFieldDegreeFormula K K' F F']
    {D : Divisor K F} (hD : D ∈ Divisor.degZero (K := K) (F := F)) :
    Divisor.pullbackConstants K' F' D ∈ Divisor.degZero (K := K') (F := F')

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