noncomputable def
RayClassField.conductorModulus
{K : Type u}
[Field K]
[NumberField K]
(p : CongruenceSubgroupPair K)
:
Modulus K
Instances For
theorem
RayClassField.conductorModulus_witness_spec
{K : Type u}
[Field K]
[NumberField K]
(p : CongruenceSubgroupPair K)
:
p.IsEquiv ⋯.choose ∧ ∀ (q : CongruenceSubgroupPair K), p.IsEquiv q → (conductorModulus p).dvd q.modulus
theorem
RayClassField.conductorModulus_dvd
{K : Type u}
[Field K]
[NumberField K]
(p : CongruenceSubgroupPair K)
:
(conductorModulus p).dvd p.modulus
theorem
RayClassField.conductorModulus_dvd_of_equiv
{K : Type u}
[Field K]
[NumberField K]
(p p' : CongruenceSubgroupPair K)
(h : p.IsEquiv p')
:
(conductorModulus p).dvd p'.modulus
theorem
RayClassField.conductorModulus_eq_of_equiv
{K : Type u}
[Field K]
[NumberField K]
(p₁ p₂ : CongruenceSubgroupPair K)
(h : p₁.IsEquiv p₂)
:
theorem
RayClassField.conductorModulus_exists_equiv
{K : Type u}
[Field K]
[NumberField K]
(p : CongruenceSubgroupPair K)
:
∃ (p' : CongruenceSubgroupPair K), p'.modulus = conductorModulus p ∧ p.IsEquiv p'
noncomputable def
RayClassField.CongruenceSubgroupPair.conductor
{K : Type u}
[Field K]
[NumberField K]
(p : CongruenceSubgroupPair K)
:
Modulus K
Instances For
def
RayClassField.CongruenceSubgroupPair.IsPrimitive
{K : Type u}
[Field K]
[NumberField K]
(p : CongruenceSubgroupPair K)
:
Instances For
theorem
RayClassField.CongruenceSubgroupPair.conductor_dvd
{K : Type u}
[Field K]
[NumberField K]
(p : CongruenceSubgroupPair K)
:
theorem
RayClassField.CongruenceSubgroupPair.conductor_dvd_of_equiv
{K : Type u}
[Field K]
[NumberField K]
(p p' : CongruenceSubgroupPair K)
(h : p.IsEquiv p')
:
theorem
RayClassField.CongruenceSubgroupPair.conductor_eq_of_equiv
{K : Type u}
[Field K]
[NumberField K]
(p₁ p₂ : CongruenceSubgroupPair K)
(h : p₁.IsEquiv p₂)
: