All.lean
Nyll.ClassFieldTheory.Definitions.HilbertSymbols.All
0 declarations indexed from sourceView source ↗
Module documentation
Hilbert symbols and Kummer norm definitions
This aggregate collects local and global Hilbert pairings and their laws, Kummer algebras and norm subgroups, and power classes.
Imports15
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.GlobalHilbertPairingFamily
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.GlobalHilbertPairingFiniteFactor
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.GlobalHilbertPairingProperties
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.GlobalInfinitePlaceHilbertSymbol
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.FinitePlaceHilbertBadSet
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.HilbertPairing
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.HilbertPairingLaws
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.HilbertPairingNormResidueCriterion
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.HilbertPairingSymbol
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.IsKummerNorm
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.IsLocalHilbertPairing
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.KummerAlgebra
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.KummerAlgebraNormSubgroup
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.PowerClass
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.PowerClassGroup
Imported by1
This module has no indexed declarations. Its imports and full source are available here.