theorem ConductorRamification.conductorVal_eq_zero_iff_unramified {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [KroneckerWeber.IsAbelianExtension K L] (𝔭 : RayClassField.Prime' K) : (GlobalCFT.extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) = 0 ↔ GlobalCFT.IsUnramifiedIn K L 𝔭

theorem ConductorRamification.conductorVal_eq_one_iff_tamelyRamified {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [KroneckerWeber.IsAbelianExtension K L] (𝔭 : RayClassField.Prime' K) : (GlobalCFT.extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) = 1 ↔ GlobalCFT.IsTamelyRamifiedIn K L 𝔭 ∧ ¬GlobalCFT.IsUnramifiedIn K L 𝔭

theorem ConductorRamification.conductorVal_ge_two_iff_wildlyRamified {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [KroneckerWeber.IsAbelianExtension K L] (𝔭 : RayClassField.Prime' K) : 2 ≤ (GlobalCFT.extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) ↔ GlobalCFT.IsWildlyRamifiedIn K L 𝔭

theorem ConductorRamification.proposition_22_25 {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [KroneckerWeber.IsAbelianExtension K L] (𝔭 : RayClassField.Prime' K) : ((GlobalCFT.extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) = 0 ↔ GlobalCFT.IsUnramifiedIn K L 𝔭) ∧ ((GlobalCFT.extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) = 1 ↔ GlobalCFT.IsTamelyRamifiedIn K L 𝔭 ∧ ¬GlobalCFT.IsUnramifiedIn K L 𝔭) ∧ (2 ≤ (GlobalCFT.extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) ↔ GlobalCFT.IsWildlyRamifiedIn K L 𝔭)