def RayClassField.RayClassChar.IsPrimitive {K : Type u} [Field K] [NumberField K] {m : Modulus K} (chi : RayClassChar K m) : Prop

theorem RayClassField.approx_theorem_local {K : Type u} [Field K] [NumberField K] (𝔪 𝔫 : Modulus K) (h : 𝔪.dvd 𝔫) (x : FracIdealsCoprime K 𝔪) : ∃ (y : FracIdealsCoprime K 𝔫), ∃ r ∈ RayGroup K 𝔪, x = (GlobalCFT.FracIdealsCoprime.inclusion K 𝔪 𝔫 h) y * r

theorem RayClassField.RayClassGroup.mapOfDvd_surjective {K : Type u} [Field K] [NumberField K] {𝔪₁ 𝔪₂ : Modulus K} (h : 𝔪₁.dvd 𝔪₂) : Function.Surjective ⇑(GlobalCFT.RayClassGroup.mapOfDvd h)

theorem RayClassField.isEquiv_kernel_of_induced {K : Type u} [Field K] [NumberField K] {m m' : Modulus K} (chi : RayClassChar K m) (chi' : RayClassChar K m') (h : m'.dvd m) (hind : GlobalCFT.IsInducedBy K m' m h chi' chi) : chi.kernelCongruenceSubgroup.IsEquiv chi'.kernelCongruenceSubgroup

theorem RayClassField.mapOfDvd_ker_le_chi_ker {K : Type u} [Field K] [NumberField K] {m : Modulus K} (chi : RayClassChar K m) : (GlobalCFT.RayClassGroup.mapOfDvd ⋯).ker ≤ MonoidHom.ker chi

theorem RayClassField.exists_primitive_inducing {K : Type u} [Field K] [NumberField K] {m : Modulus K} (chi : RayClassChar K m) : ∃ (chi_prim : RayClassChar K chi.conductor), chi_prim.kernelCongruenceSubgroup.IsPrimitive ∧ GlobalCFT.IsInducedBy K chi.conductor m ⋯ chi_prim chi

theorem RayClassField.kernel_isPrimitive_iff_modulus_eq_conductor {K : Type u} [Field K] [NumberField K] {m : Modulus K} (chi : RayClassChar K m) : chi.kernelCongruenceSubgroup.IsPrimitive ↔ m = chi.conductor

theorem RayClassField.conductor_dvd_of_inducing {K : Type u} [Field K] [NumberField K] {m m' : Modulus K} (chi : RayClassChar K m) (chi' : RayClassChar K m') (h : m'.dvd m) (hind : GlobalCFT.IsInducedBy K m' m h chi' chi) : chi.conductor.dvd m'

theorem RayClassField.RayClassChar.isPrimitive_iff_kernel_isPrimitive {K : Type u} [Field K] [NumberField K] {m : Modulus K} (chi : RayClassChar K m) : chi.IsPrimitive ↔ chi.kernelCongruenceSubgroup.IsPrimitive