All.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.All
0 declarations indexed from sourceView source ↗
Module documentation
Ramification of number fields
Public aggregate for finite ramification support, rational prime ideals, everywhere-unramified rational extensions, and global degree bounds.
Imports6
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.DegreeFromChosenPrimes
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.DegreeProduct
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.FiniteRamifiedPrimes
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.RationalPrime
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.Splitting.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.UnramifiedRationals
Imported by1
This module has no indexed declarations. Its imports and full source are available here.