NYLL
Module

WeilDatum_pairing_ne_zero.lean

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

Module documentation

Disjoint rational supports make both divisor evaluations, and hence the Weil pairing, nonzero.

Imports3
Imported by2

Declarations

theorem

ord_f₁_eq_zero_of_mem_support'

L37 ↗
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.WeilDatum_pairing_ne_zero
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'

L43 ↗
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.WeilDatum_pairing_ne_zero
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'

L49 ↗
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.WeilDatum_pairing_ne_zero
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'

L55 ↗
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.WeilDatum_pairing_ne_zero
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'

L61 ↗
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.WeilDatum_pairing_ne_zero
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'

L68 ↗
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.WeilDatum_pairing_ne_zero
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'

L75 ↗
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.WeilDatum_pairing_ne_zero
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 _root_.AlgebraicCurve.WeilDatum.evalFun_f₁_ne_zero' :
    Divisor.evalFun d.f₁ d.D₂ ≠ 0
theorem

evalFun_f₂_ne_zero'

L80 ↗
AlgebraicCurve.WeilDatum.evalFun_f₂_ne_zero'
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_ne_zero
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
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.evalFun_f₂_ne_zero' :
    Divisor.evalFun d.f₂ d.D₁ ≠ 0
theorem

pairing_ne_zero

L89 ↗
AlgebraicCurve.WeilDatum.pairing_ne_zero
Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_ne_zero
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve in
open JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_ne_zero.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.pairing_ne_zero {K F : Type*} [Field K] [Field F]
    [Algebra K F] {n : ℕ} (d : WeilDatum K F n) : d.pairing ≠ 0

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