All.lean
Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.All
0 declarations indexed from sourceView source ↗
Module documentation
Conductors and ray class-field definitions
This aggregate collects conductor and modulus conditions, ray class groups and realizations, ideal norms, and ray Artin maps.
Imports21
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.EmbedsInRayClassField
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.FractionalIdealNormExponentMap
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.FractionalIdealNorm
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.IsAbelianConductor
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.IsRayCongruent
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.IsUnramifiedOutsideModulus
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.NarrowClassGroup
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.NarrowRayClassModulus
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.OrdinaryRayClassModulus
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayArtin
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassFieldRealization
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassGroup
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassIdealModulusProjection
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassIdealNorm
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassModulus
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassOfFinitePrime
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassPrimeToIdeals
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassSubgroupRealization
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassSubgroupQuotientEquiv
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayLocalHigherUnitGroup
- Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayPrincipalIdealSubgroup
Imported by1
This module has no indexed declarations. Its imports and full source are available here.