All.lean
Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.All
0 declarations indexed from sourceView source ↗
Module documentation
Local Kummer reciprocity
Aggregate for the local Hilbert symbol, its laws, and the maximal local Kummer pairing, including the tame power-residue formula.
Imports12
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.CanonicalKummerNorm
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.KummerExponentTower
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.KummerNormPowerClassDegree
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertExponentCompatibility
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertPairing
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertPairingNondegeneracy
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertSymbol
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertSymbolLaws
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.MathlibHilbertPairing
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.MaximalLocalKummerPairing
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.PowerResidueTameFormula
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.SmallHilbertPairingTransport
Imported by1
This module has no indexed declarations. Its imports and full source are available here.