Every number field has a ramified prime over ℚ

...except ℚ itself.

This is a trivial corollary of NumberField.not_dvd_discr_iff_forall_mem and NumberField.abs_discr_gt_two but is placed in a separate file to avoid large imports.

theorem NumberField.exists_not_isUnramifiedIn {K : Type u_1} {𝒪 : Type u_2} [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsIntegralClosure 𝒪 ℤ K] (H : Module.finrank ℚ K ≠ 1) : ∃ (p : ℕ), Nat.Prime p ∧ ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})

If K is a number field with positive rank, then some prime is ramified in K.

theorem NumberField.exists_not_isUnramifiedAt_int {K : Type u_1} {𝒪 : Type u_2} [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsIntegralClosure 𝒪 ℤ K] (H : Module.finrank ℚ K ≠ 1) : ∃ (P : Ideal 𝒪) (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

If K is a number field with positive rank, then there exists some maximal ideal of 𝓞 K that is ramified over ℤ.

theorem NumberField.finrank_eq_one_of_unramified {K : Type u_1} {𝒪 : Type u_2} [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsIntegralClosure 𝒪 ℤ K] [Algebra.Unramified ℤ 𝒪] : Module.finrank ℚ K = 1

Any number field that is unramified over ℚ has rank 1.

theorem bijective_algebraMap_int_of_finite_of_unramified {𝒪 : Type u_2} [CommRing 𝒪] [Module.Finite ℤ 𝒪] [Algebra.Unramified ℤ 𝒪] [IsDomain 𝒪] [FaithfulSMul ℤ 𝒪] : Function.Bijective ⇑(algebraMap ℤ 𝒪)

If 𝒪 is a domain that is a finite and unramified extension of ℤ, then 𝒪 = ℤ.

theorem NumberField.exists_not_isUnramifiedAt_int_of_isGalois {K : Type u_1} {𝒪 : Type u_2} [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsIntegralClosure 𝒪 ℤ K] [IsGalois ℚ K] (H : 1 < Module.finrank ℚ K) : ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P

If K is a number field with positive rank such that K/ℚ is galois, then there exists some rational prime p : ℕ such that every prime of K over p is ramified.