Module

IsRayCongruentOfLe.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.IsRayCongruentOfLe

1 declaration indexed from sourceView source ↗

Module documentation

Ray congruence under enlargement of the modulus

A larger modulus has at least as strong a congruence condition at each finite prime and at least as many real positivity conditions.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

of_le

L29 ↗

ClassFieldTheory.IsRayCongruent.of_le

Documentation

An element ray-congruent for a larger modulus is ray-congruent for a smaller modulus.

Source context 5 commands

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

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

Lean source · statement

theorem of_le
    {K : Type u} [Field K] [NumberField K]
    {m n : RayClassModulus K} (hmn : m ≤ n)
    {x : Kˣ} (hx : IsRayCongruent n x) :
    IsRayCongruent m x

Module documentation

Ray congruence under enlargement of the modulus

Declarations

of_le