ClassFieldTheory.rayPrincipalIdealSubgroup_le_primeToIdeals
A ray-principal fractional ideal has zero exponent at every finite prime in the modulus support.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
universe uLean source · statement
theorem rayPrincipalIdealSubgroup_le_primeToIdeals
(K : Type u) [Field K] [NumberField K]
(m : RayClassModulus K) :
rayPrincipalIdealSubgroup m ≤ rayClassPrimeToIdeals m