NYLL
Module

RayPrincipalIdealSubgroup.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayPrincipalIdealSubgroup
2 declarations indexed from sourceView source ↗

Module documentation

Ray-principal ideals

Imports3
Imported by6

Declarations

def

rayPrincipalIdealSubgroup

L26 ↗
ClassFieldTheory.rayPrincipalIdealSubgroup
Documentation

The subgroup generated by principal fractional ideals whose generators satisfy the ray congruence.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField
namespace ClassFieldTheory
universe u
Lean source · statement
def rayPrincipalIdealSubgroup
    {K : Type u} [Field K] [NumberField K]
    (m : RayClassModulus K) :
    Subgroup (NumberFieldFractionalIdealGroup K)
def

rayPrincipalIdealSubgroupInPrimeTo

L36 ↗
ClassFieldTheory.rayPrincipalIdealSubgroupInPrimeTo
Documentation

Ray-principal ideals, restricted to the group of ideals prime to the modulus.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField
namespace ClassFieldTheory
universe u
Lean source · statement
def rayPrincipalIdealSubgroupInPrimeTo
    {K : Type u} [Field K] [NumberField K]
    (m : RayClassModulus K) :
    Subgroup (rayClassPrimeToIdeals m)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.