ClassFieldTheory.rayClassPrimeToIdeals
The subgroup of nonzero fractional ideals prime to the finite part of a ray modulus.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe uLean source · full declaration
def rayClassPrimeToIdeals
{K : Type u} [Field K] [NumberField K]
(m : RayClassModulus K) :
Subgroup (NumberFieldFractionalIdealGroup K) where
carrier := {I | ∀ v, v ∈ m.finitePart.support →
FractionalIdeal.count K v
(I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) = 0}
one_mem' v _ := FractionalIdeal.count_one K v
mul_mem' {I J} hI hJ v hv := by
rw [Units.val_mul,
FractionalIdeal.count_mul K v (Units.ne_zero I) (Units.ne_zero J),
hI v hv, hJ v hv, add_zero]
inv_mem' {I} hI v hv := by
rw [Units.val_inv_eq_inv_val, FractionalIdeal.count_inv K v,
hI v hv, neg_zero]