NYLL
Module

Card_effectiveDivisors_mul_eq_sum.lean

Nyll.AlgebraicCurves.Divisors.Card_effectiveDivisors_mul_eq_sum
9 declarations indexed from sourceView source ↗

Module documentation

Card effective Divisors mul eq sum

Imports5
Imported by1

Declarations

theorem

degree_eq_sum

L52 ↗
AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum.AlgebraicCurve.CardEffectiveDivisorsSol.degree_eq_sum
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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 AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
open _root_.AlgebraicCurve
open _root_.Finset
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardEffectiveDivisorsSol
open _root_.AlgebraicCurve
Lean source · statement
theorem degree_eq_sum {K F : Type*} [Field K] [Field F] [Algebra K F]
    (D : Divisor K F) {S : Finset (Place K F)} (hS : D.support ⊆ S) :
    Divisor.degree D = ∑ v ∈ S, D v * (v.deg : ℤ)
theorem

apply_mul_deg_le_degree

L60 ↗
AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum.AlgebraicCurve.CardEffectiveDivisorsSol.apply_mul_deg_le_degree
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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 AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
open _root_.AlgebraicCurve
open _root_.Finset
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardEffectiveDivisorsSol
open _root_.AlgebraicCurve
Lean source · statement
theorem apply_mul_deg_le_degree {K F : Type*} [Field K] [Field F] [Algebra K F]
    (D : Divisor K F) (hD : ∀ v, 0 ≤ D v) (v : Place K F) :
    D v * (v.deg : ℤ) ≤ Divisor.degree D
theorem

deg_le_of_mem_support

L68 ↗
AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum.AlgebraicCurve.CardEffectiveDivisorsSol.deg_le_of_mem_support
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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 AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
open _root_.AlgebraicCurve
open _root_.Finset
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardEffectiveDivisorsSol
open _root_.AlgebraicCurve
Lean source · statement
theorem deg_le_of_mem_support {K F : Type*} [Field K] [Field F] [Algebra K F]
    (D : Divisor K F) (hD : ∀ v, 0 ≤ D v) {m : ℕ} (hdeg : Divisor.degree D = (m : ℤ))
    {v : Place K F} (hv : v ∈ D.support) : v.deg ≤ m
theorem

card_eff_sub_eq_card_filter

L80 ↗
AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum.AlgebraicCurve.CardEffectiveDivisorsSol.card_eff_sub_eq_card_filter
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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 AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
open _root_.AlgebraicCurve
open _root_.Finset
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardEffectiveDivisorsSol
open _root_.AlgebraicCurve
Lean source · full declaration
theorem card_eff_sub_eq_card_filter {K F : Type*} [Field K] [Field F] [Algebra K F]
    (n m : ℕ) (v : Place K F) (hm : m * v.deg ≤ n) (En Em : Finset (Divisor K F))
    (hEn : ∀ D, D ∈ En ↔ 0 ≤ D ∧ Divisor.degree D = (n : ℤ))
    (hEm : ∀ D, D ∈ Em ↔ 0 ≤ D ∧ Divisor.degree D = ((n - m * v.deg : ℕ) : ℤ)) :
    Em.card = (En.filter fun D => (m : ℤ) ≤ D v).card := by
  classical
  have hcast : ((n - m * v.deg : ℕ) : ℤ) = (n : ℤ) - (m : ℤ) * (v.deg : ℤ) := by
    rw [Nat.cast_sub hm, Nat.cast_mul]
  have hsingle : ∀ w, 0 ≤ (Finsupp.single v (m : ℤ)) w := fun w => by
    rw [Finsupp.single_apply]
    split_ifs <;> simp
  refine Finset.card_nbij' (fun D => D + Finsupp.single v (m : ℤ))
    (fun D => D - Finsupp.single v (m : ℤ)) ?_ ?_ ?_ ?_
  · intro D hD
    rw [Finset.mem_coe, hEm] at hD
    obtain ⟨hD0, hDdeg⟩ := hD
    rw [Finsupp.le_def] at hD0
    rw [Finset.mem_coe, Finset.mem_filter, hEn, Finsupp.le_def]
    refine ⟨⟨fun w => ?_, ?_⟩, ?_⟩
    · have h1 := hD0 w
      have h2 := hsingle w
      simp only [Finsupp.coe_zero, Pi.zero_apply, Finsupp.coe_add, Pi.add_apply] at h1 ⊢
      linarith
    · rw [map_add, hDdeg, Divisor.degree_single, hcast]
      ring
    · have h1 := hD0 v
      simp only [Finsupp.coe_zero, Pi.zero_apply, Finsupp.coe_add, Pi.add_apply,
        Finsupp.single_eq_same] at h1 ⊢
      linarith
  · intro D hD
    rw [Finset.mem_coe, Finset.mem_filter, hEn, Finsupp.le_def] at hD
    obtain ⟨⟨hD0, hDdeg⟩, hmv⟩ := hD
    rw [Finset.mem_coe, hEm, Finsupp.le_def]
    refine ⟨fun w => ?_, ?_⟩
    · have h1 := hD0 w
      simp only [Finsupp.coe_zero, Pi.zero_apply, Finsupp.coe_sub, Pi.sub_apply] at h1 ⊢
      rw [Finsupp.single_apply]
      split_ifs with hw
      · subst hw
        linarith
      · linarith
    · rw [map_sub, hDdeg, Divisor.degree_single, hcast]
  · intro D _
    simp
  · intro D _
    simp
theorem

one_le_deg

L133 ↗
AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum.AlgebraicCurve.CardEffectiveDivisorsSol.one_le_deg
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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 AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
open _root_.AlgebraicCurve
open _root_.Finset
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardEffectiveDivisorsSol
open _root_.AlgebraicCurve
section Finite
variable {K F : Type*} [Field K] [Finite K] [Field F] [Algebra K F]
  [IsCurveOver K F] [Algebra.EssFiniteType K F]
omit [Finite K] [Algebra.EssFiniteType K F] in
Lean source · statement
theorem one_le_deg (v : Place K F) : 1 ≤ v.deg
theorem

finite_setOf_deg_le

L138 ↗
AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum.AlgebraicCurve.CardEffectiveDivisorsSol.finite_setOf_deg_le
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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 AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
open _root_.AlgebraicCurve
open _root_.Finset
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardEffectiveDivisorsSol
open _root_.AlgebraicCurve
section Finite
variable {K F : Type*} [Field K] [Finite K] [Field F] [Algebra K F]
  [IsCurveOver K F] [Algebra.EssFiniteType K F]
Lean source · statement
theorem finite_setOf_deg_le (n : ℕ) : {v : Place K F | v.deg ≤ n}.Finite
theorem

finite_eff

L146 ↗
AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum.AlgebraicCurve.CardEffectiveDivisorsSol.finite_eff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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 AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
open _root_.AlgebraicCurve
open _root_.Finset
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardEffectiveDivisorsSol
open _root_.AlgebraicCurve
section Finite
variable {K F : Type*} [Field K] [Finite K] [Field F] [Algebra K F]
  [IsCurveOver K F] [Algebra.EssFiniteType K F]
Lean source · statement
theorem finite_eff (m : ℕ) :
    {D : Divisor K F | 0 ≤ D ∧ Divisor.degree D = (m : ℤ)}.Finite
theorem

main

L179 ↗
AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum.AlgebraicCurve.CardEffectiveDivisorsSol.main
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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 AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
open _root_.AlgebraicCurve
open _root_.Finset
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardEffectiveDivisorsSol
open _root_.AlgebraicCurve
section Finite
variable {K F : Type*} [Field K] [Finite K] [Field F] [Algebra K F]
  [IsCurveOver K F] [Algebra.EssFiniteType K F]
Lean source · statement
theorem main (n : ℕ) :
    n * Nat.card {D : Divisor K F // 0 ≤ D ∧ Divisor.degree D = (n : ℤ)} =
      ∑ r ∈ Finset.Icc 1 n,
        (∑ d ∈ Nat.divisors r, d * Nat.card {v : Place K F | v.deg = d}) *
          Nat.card {D : Divisor K F // 0 ≤ D ∧ Divisor.degree D = ((n - r : ℕ) : ℤ)}
theorem

card_effectiveDivisors_mul_eq_sum

L334 ↗
AlgebraicCurve.card_effectiveDivisors_mul_eq_sum
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effectiveDivisors_mul_eq_sum
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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 AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
open _root_.AlgebraicCurve
open _root_.Finset
Lean source · statement
theorem _root_.AlgebraicCurve.card_effectiveDivisors_mul_eq_sum
    (k F : Type*) [Field k] [Finite k] [Field F] [Algebra k F]
    [AlgebraicCurve.IsCurveOver k F] [Algebra.EssFiniteType k F] (n : ℕ) :
    n * Nat.card {D : AlgebraicCurve.Divisor k F //
        0 ≤ D ∧ AlgebraicCurve.Divisor.degree D = (n : ℤ)} =
      ∑ r ∈ Finset.Icc 1 n,
        (∑ d ∈ Nat.divisors r, d * Nat.card {v : AlgebraicCurve.Place k F | v.deg = d}) *
          Nat.card {D : AlgebraicCurve.Divisor k F //
            0 ≤ D ∧ AlgebraicCurve.Divisor.degree D = ((n - r : ℕ) : ℤ)}

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