NYLL
Module

WeilDatum_addLeft_pairing.lean

Nyll.JacobianVarieties.WeilPairing.WeilDatum_addLeft_pairing
9 declarations indexed from sourceView source ↗

Module documentation

Multiplicativity of the Weil pairing in the left argument

Imports6
Imported by2

Declarations

theorem

ord_f₁_eq_zero_of_mem_support'

L40 ↗
AlgebraicCurve.WeilDatum.ord_f₁_eq_zero_of_mem_support'
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilAddLeft
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} (d : WeilDatum K F n)
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.ord_f₁_eq_zero_of_mem_support'
    {v : Place K F} (hv : v ∈ d.D₂.support) :
    v.ord d.f₁ = 0
theorem

ord_f₂_eq_zero_of_mem_support'

L46 ↗
AlgebraicCurve.WeilDatum.ord_f₂_eq_zero_of_mem_support'
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilAddLeft
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} (d : WeilDatum K F n)
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.ord_f₂_eq_zero_of_mem_support'
    {v : Place K F} (hv : v ∈ d.D₁.support) :
    v.ord d.f₂ = 0
theorem

rational_of_mem_support_left'

L52 ↗
AlgebraicCurve.WeilDatum.rational_of_mem_support_left'
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilAddLeft
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} (d : WeilDatum K F n)
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.rational_of_mem_support_left'
    {v : Place K F} (hv : v ∈ d.D₁.support) :
    v.IsRational
theorem

rational_of_mem_support_right'

L58 ↗
AlgebraicCurve.WeilDatum.rational_of_mem_support_right'
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilAddLeft
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} (d : WeilDatum K F n)
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.rational_of_mem_support_right'
    {v : Place K F} (hv : v ∈ d.D₂.support) :
    v.IsRational
theorem

evalAt_f₁_ne_zero'

L64 ↗
AlgebraicCurve.WeilDatum.evalAt_f₁_ne_zero'
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilAddLeft
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} (d : WeilDatum K F n)
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.evalAt_f₁_ne_zero'
    {v : Place K F} (hv : v ∈ d.D₂.support) :
    v.evalAt d.f₁ ≠ 0
theorem

evalAt_f₂_ne_zero'

L71 ↗
AlgebraicCurve.WeilDatum.evalAt_f₂_ne_zero'
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilAddLeft
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} (d : WeilDatum K F n)
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.evalAt_f₂_ne_zero'
    {v : Place K F} (hv : v ∈ d.D₁.support) :
    v.evalAt d.f₂ ≠ 0
theorem

evalFun_f₁_ne_zero'

L78 ↗
JacobianVarieties.WeilPairing.Proofs.WeilAddLeft.AlgebraicCurve.WeilDatum.evalFun_f₁_ne_zero'
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilAddLeft
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} (d : WeilDatum K F n)
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem evalFun_f₁_ne_zero' : Divisor.evalFun d.f₁ d.D₂ ≠ 0
theorem

evalFun_f₂_ne_zero'

L81 ↗
JacobianVarieties.WeilPairing.Proofs.WeilAddLeft.AlgebraicCurve.WeilDatum.evalFun_f₂_ne_zero'
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilAddLeft
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} (d : WeilDatum K F n)
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem evalFun_f₂_ne_zero' : Divisor.evalFun d.f₂ d.D₁ ≠ 0
theorem

addLeft_pairing

L88 ↗
AlgebraicCurve.WeilDatum.addLeft_pairing
Source context 4 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilAddLeft
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
  _root_.JacobianVarieties.WeilPairing.Proofs.WeilAddLeft.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.addLeft_pairing
    {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ}
    (d d' : WeilDatum K F n) (hD : d.D₂ = d'.D₂) (hf : d.f₂ = d'.f₂) :
    (d.addLeft d' hD hf).pairing = d.pairing * d'.pairing

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