NYLL
Module

WeilDatum_symm_pairing.lean

Nyll.JacobianVarieties.WeilPairing.WeilDatum_symm_pairing
1 declaration indexed from sourceView source ↗

Module documentation

Interchanging the two divisors in Weil pairing data inverts the pairing.

Imports1
Imported by3

Declarations

theorem

symm_pairing

L25 ↗
AlgebraicCurve.WeilDatum.symm_pairing
Source context 3 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_symm_pairing
open AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.symm_pairing {K F : Type*} [Field K] [Field F] [Algebra K F]
    {n : ℕ} (d : WeilDatum K F n) : d.symm.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.