Module

NumberFieldFractionalIdealGroup.lean

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.NumberFieldFractionalIdealGroup

1 declaration indexed from sourceView source ↗

Module documentation

Fractional-ideal group of a number field

Imports2

Mathlib.NumberTheory.NumberField.Basic
Mathlib.RingTheory.ClassGroup.Basic

Imported by5

abbrev

NumberFieldFractionalIdealGroup

ClassFieldTheory.NumberFieldFractionalIdealGroup

Documentation

The group of nonzero fractional ideals of a number field.

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

abbrev NumberFieldFractionalIdealGroup
    (K : Type u) [Field K] [NumberField K]