def LocalConductor.IsArchimedeanLocalField (K : Type u_1) [IsLocalField K] : Prop

def LocalConductor.IsNonarchimedeanLocalField (K : Type u_1) [IsLocalField K] : Prop

noncomputable def LocalConductor.archLocalConductor (K : Type u_1) (L : Type u_2) [IsLocalField K] [IsLocalField L] [Algebra K L] [FiniteDimensional K L] (_hK : IsArchimedeanLocalField K) : ℕ

def LocalConductor.higherUnitGroupSet (K : Type u_1) [IsLocalField K] (_hK : IsNonarchimedeanLocalField K) (n : ℕ) : Set K

def LocalConductor.HigherUnitsInNormGroup (K : Type u_1) (L : Type u_2) [IsLocalField K] [IsLocalField L] [Algebra K L] [FiniteDimensional K L] (hK : IsNonarchimedeanLocalField K) (n : ℕ) : Prop

theorem LocalConductor.HigherUnitsInNormGroup_exists (K : Type u_1) (L : Type u_2) [IsLocalField K] [IsLocalField L] [Algebra K L] [FiniteDimensional K L] (hK : IsNonarchimedeanLocalField K) : ∃ (n : ℕ), HigherUnitsInNormGroup K L hK n

noncomputable def LocalConductor.nonarchLocalConductor (K : Type u_1) (L : Type u_2) [IsLocalField K] [IsLocalField L] [Algebra K L] [FiniteDimensional K L] (hK : IsNonarchimedeanLocalField K) : ℕ

noncomputable def LocalConductor.localConductor (K : Type u_1) (L : Type u_2) [IsLocalField K] [IsLocalField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : ℕ

theorem LocalConductor.HigherUnitsInNormGroup_of_sub (K : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [IsLocalField K] [IsLocalField L₁] [IsLocalField L₂] [Algebra K L₁] [FiniteDimensional K L₁] [IsGalois K L₁] [Algebra K L₂] [FiniteDimensional K L₂] [IsGalois K L₂] (hK : IsNonarchimedeanLocalField K) (f : L₁ →ₐ[K] L₂) (n : ℕ) : HigherUnitsInNormGroup K L₂ hK n → HigherUnitsInNormGroup K L₁ hK n

theorem LocalConductor.finrank_ne_one_of_sub (K : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [Field K] [Field L₁] [Field L₂] [Algebra K L₁] [FiniteDimensional K L₁] [Algebra K L₂] [FiniteDimensional K L₂] (f : L₁ →ₐ[K] L₂) (h : Module.finrank K L₁ ≠ 1) : Module.finrank K L₂ ≠ 1

noncomputable def GlobalConductor.localNormImage (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Set (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭)

def GlobalConductor.FinitePlaceHigherUnitsInNormGroup (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ℕ → Prop

theorem GlobalConductor.FinitePlaceHigherUnitsInNormGroup_exists (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ∃ (n : ℕ), FinitePlaceHigherUnitsInNormGroup K L 𝔭 n

theorem GlobalConductor.FinitePlaceHigherUnitsInNormGroup_zero_of_unramified (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (h : GlobalCFT.IsUnramifiedIn K L 𝔭) : FinitePlaceHigherUnitsInNormGroup K L 𝔭 0

noncomputable def GlobalConductor.localConductorAtFinitePlace (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ℕ

noncomputable def GlobalConductor.localConductorAtInfinitePlace (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (v : NumberField.InfinitePlace K) : ℕ

theorem GlobalConductor.localConductorAtInfinitePlace_le_one (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (v : NumberField.InfinitePlace K) : localConductorAtInfinitePlace K L v ≤ 1

theorem GlobalConductor.localConductorAtInfinitePlace_complex (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (v : NumberField.InfinitePlace K) (hv : v.IsComplex) : localConductorAtInfinitePlace K L v = 0

theorem GlobalConductor.finite_ramified_primes (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) | ¬GlobalCFT.IsUnramifiedIn K L 𝔭}.Finite

theorem GlobalConductor.localConductorAtFinitePlace_finite_support (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) | localConductorAtFinitePlace K L 𝔭 ≠ 0}.Finite

theorem GlobalConductor.conductorFiniteSupport (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : {v : RayClassField.Place K | (match v with | RayClassField.Place.finite 𝔭 => localConductorAtFinitePlace K L 𝔭 | RayClassField.Place.infinite w => localConductorAtInfinitePlace K L w) ≠ 0}.Finite

noncomputable def GlobalConductor.conductorModulus (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : RayClassField.Modulus K

theorem GlobalConductor.conductorModulus_eq_extensionConductor (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : conductorModulus K L = GlobalCFT.extensionConductor K L

theorem GlobalConductor.localNormImage_mono (K L₁ L₂ : Type u) [Field K] [NumberField K] [Field L₁] [NumberField L₁] [Algebra K L₁] [FiniteDimensional K L₁] [IsGalois K L₁] [Field L₂] [NumberField L₂] [Algebra K L₂] [FiniteDimensional K L₂] [IsGalois K L₂] (f : L₁ →ₐ[K] L₂) (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : localNormImage K L₂ 𝔭 ⊆ localNormImage K L₁ 𝔭

theorem GlobalConductor.FinitePlaceHigherUnitsInNormGroup_of_sub (K L₁ L₂ : Type u) [Field K] [NumberField K] [Field L₁] [NumberField L₁] [Algebra K L₁] [FiniteDimensional K L₁] [IsGalois K L₁] [Field L₂] [NumberField L₂] [Algebra K L₂] [FiniteDimensional K L₂] [IsGalois K L₂] (f : L₁ →ₐ[K] L₂) (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (n : ℕ) : FinitePlaceHigherUnitsInNormGroup K L₂ 𝔭 n → FinitePlaceHigherUnitsInNormGroup K L₁ 𝔭 n