All.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.All
0 declarations indexed from sourceView source ↗
Module documentation
Finite and everywhere-unramified towers of number fields
Imports16
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.CompletelySplitPrimes
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.CompletelySplitPrimesModFour
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.DegreeOnePrimes
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.IntegralPrimitiveElement
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.PlaceEquiv
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.SchurPrimeDivisors
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.EverywhereUnramifiedTower
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.FiniteUnramifiedEtaleBridge
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.FiniteUnramifiedTower
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.MathlibUnramifiedInterface
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.CompletelySplitFinset
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.GaloisDifferentBound
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.RootDiscriminantBound
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.SmallModel
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.SupportedDiscriminantBound
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.TameDifferentTrace
Imported by1
This module has no indexed declarations. Its imports and full source are available here.