All.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.All
0 declarations indexed from sourceView source ↗
Module documentation
Ray class groups
Public aggregate for approximation, congruence subgroups, and ray class groups of number fields.
Imports12
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Approximation
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Basic
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.FullModulus
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Ideal
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.IdealNorm
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.LocalConductor
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Narrow
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.OrdinaryClassGroupComparison
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.PrimeGeneration
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.PublicHigherUnitComparison
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Rational
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Topology
Imported by1
This module has no indexed declarations. Its imports and full source are available here.