Module

HilbertPairingLaws.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.HilbertPairingLaws

3 declarations indexed from sourceView source ↗

Module documentation

Imports1

Imported by2

def

ClassFieldTheory.HilbertPairing.IsSteinberg

Documentation

The Steinberg relation for a pairing on power classes.

Source context 2 commands

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

namespace ClassFieldTheory.HilbertPairing
universe u

Lean source · statement

def IsSteinberg
    {K : Type u} [Field K] {n : ℕ+}
    (B : HilbertPairing K n) : Prop

def

ClassFieldTheory.HilbertPairing.IsSkewSymmetric

Documentation

Skew-symmetry of a pairing on power classes.

Source context 2 commands

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

namespace ClassFieldTheory.HilbertPairing
universe u

Lean source · statement

def IsSkewSymmetric
    {K : Type u} [Field K] {n : ℕ+}
    (B : HilbertPairing K n) : Prop

def

ClassFieldTheory.HilbertPairing.IsNondegenerate

Documentation

Nondegeneracy in both variables of a pairing on power classes.

Source context 2 commands

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

namespace ClassFieldTheory.HilbertPairing
universe u

Lean source · statement

def IsNondegenerate
    {K : Type u} [Field K] {n : ℕ+}
    (B : HilbertPairing K n) : Prop