Module

FinitePrimeFractionalIdeal.lean

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.FinitePrimeFractionalIdeal

1 declaration indexed from sourceView source ↗

Module documentation

Imports3

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.NumberFieldFractionalIdealGroup
Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Mathlib.RingTheory.DedekindDomain.Factorization

Imported by7

def

ClassFieldTheory.finitePrimeFractionalIdeal

Documentation

The nonzero fractional ideal represented by a finite prime.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

def finitePrimeFractionalIdeal
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    NumberFieldFractionalIdealGroup K