Module

HilbertPairingNormResidueCriterion.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.HilbertPairingNormResidueCriterion

1 declaration indexed from sourceView source ↗

Module documentation

Imports2

Imported by2

def

ClassFieldTheory.HilbertPairing.SatisfiesNormResidueCriterion

Documentation

The symbol of a and b is one exactly when b is a norm from the Kummer algebra of a.

Source context 2 commands

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

namespace ClassFieldTheory.HilbertPairing
universe u

Lean source · statement

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