NYLL
Module

RayPrincipalIdealMembership.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayPrincipalIdealMembership
1 declaration indexed from sourceView source ↗

Module documentation

Membership in the ray-principal ideal subgroup

The ray-congruent generators already form a subgroup under the principal ideal map, so taking their subgroup closure adds no new ideals.

Imports2
Imported by3

Declarations

theorem

mem_rayPrincipalIdealSubgroup_iff

L28 ↗
ClassFieldTheory.mem_rayPrincipalIdealSubgroup_iff
Documentation

A fractional ideal is ray-principal exactly when it has one ray-congruent nonzero generator.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace ClassFieldTheory
universe u
Lean source · statement
theorem mem_rayPrincipalIdealSubgroup_iff
    {K : Type u} [Field K] [NumberField K]
    (m : RayClassModulus K)
    (I : NumberFieldFractionalIdealGroup K) :
    I ∈ rayPrincipalIdealSubgroup m ↔
      ∃ x : Kˣ, IsRayCongruent m x ∧
        toPrincipalIdeal (𝓞 K) K x = I

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