theorem GlobalConductor.localConductorAtFinitePlace_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)) : localConductorAtFinitePlace K L₁ 𝔭 ≤ localConductorAtFinitePlace K L₂ 𝔭

theorem GlobalConductor.localConductorAtInfinitePlace_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₂) (v : NumberField.InfinitePlace K) : localConductorAtInfinitePlace K L₁ v ≤ localConductorAtInfinitePlace K L₂ v

theorem GlobalConductor.conductorModulus_dvd_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₂) : (conductorModulus K L₁).dvd (conductorModulus K L₂)

theorem GlobalConductor.lemma_22_26 (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₂) : (GlobalCFT.extensionConductor K L₁).dvd (GlobalCFT.extensionConductor K L₂)