All.lean
Nyll.ClassFieldTheory.Definitions.All
0 declarations indexed from sourceView source ↗
Module documentation
Class field theory definitions
Reader-facing vocabulary used by the headline theorem modules. Primitive leaves import Mathlib only; derived leaves import only the prerequisite definition leaves. Topic-level All modules and this root module are aggregation-only, and no public definition imports an implementation module.
Imports7
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.All
- Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.All
- Nyll.ClassFieldTheory.Definitions.GlobalClassFieldTheory.All
- Nyll.ClassFieldTheory.Definitions.HasseArf.All
- Nyll.ClassFieldTheory.Definitions.HilbertSymbols.All
- Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.All
- Nyll.ClassFieldTheory.Definitions.NormTheorems.All
Imported by1
This module has no indexed declarations. Its imports and full source are available here.