NYLL
Module

RayClassGroup.lean

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

Module documentation

Ideal-theoretic ray class groups

Imports3
Imported by14

Declarations

abbrev

RayClassGroup

L22 ↗
ClassFieldTheory.RayClassGroup
Documentation

The ideal-theoretic ray class group of a modulus.

Source context 2 commands

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

namespace ClassFieldTheory
universe u
Lean source · statement
abbrev RayClassGroup
    {K : Type u} [Field K] [NumberField K]
    (m : RayClassModulus K)
instance

instIsMulCommutativeRayClassGroup

L28 ↗
ClassFieldTheory.instIsMulCommutativeRayClassGroup
Documentation

Ray class groups are multiplicatively commutative.

Source context 2 commands

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

namespace ClassFieldTheory
universe u
Lean source · statement
instance instIsMulCommutativeRayClassGroup
    {K : Type u} [Field K] [NumberField K]
    (m : RayClassModulus K) : IsMulCommutative (RayClassGroup m)

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