NYLL
Module

Divisor_evalFun_algebraMap_pushforward.lean

Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_algebraMap_pushforward
2 declarations indexed from sourceView source ↗

Module documentation

Divisor eval Fun algebra Map pushforward

Imports7
Imported by8

Declarations

theorem

zpow_finset_sum'

L31 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_algebraMap_pushforward.zpow_finset_sum'
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_algebraMap_pushforward
open AlgebraicCurve AlgebraicCurve.Divisor
Lean source · statement
theorem zpow_finset_sum' {K : Type*} [Field K] {c : K} (hc : c ≠ 0) {ι : Type*}
    (s : Finset ι) (n : ι → ℤ) : ∏ i ∈ s, c ^ n i = c ^ (∑ i ∈ s, n i)
theorem

evalFun_algebraMap_pushforward

L38 ↗
AlgebraicCurve.Divisor.evalFun_algebraMap_pushforward
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_algebraMap_pushforward
open AlgebraicCurve AlgebraicCurve.Divisor
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.evalFun_algebraMap_pushforward {K F F' : Type*} [Field K]
  [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] {g : F} (hg : g ≠ 0) (D : Divisor K F') (hratw : ∀ w ∈ D.support,
  Place.IsRational w) (hratv : ∀ w ∈ D.support, (w.restrict F).IsRational) (hord : ∀ w ∈ D.support,
  (w.restrict F).ord g = 0) : Divisor.evalFun (algebraMap F F' g) D = Divisor.evalFun g
  (Divisor.pushforward F D)

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