Theorems · Theorem · number theory

NumberField.exists_not_isUnramifiedAt_int_of_isGalois

∀ {K : Type u_1} {𝒪 : Type u_2} [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsIntegralClosure 𝒪 ℤ K] [IsGalois ℚ K],
  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.

Defined in

Mathlib.NumberTheory.NumberField.ExistsRamified

Cited by

0 results in Mathlib

Foundations

Depth 319 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberFieldCommRingAlgebraIsIntegralClosureIsGalois