Theorems · Theorem · number theory

NumberField.not_dvd_discr_iff_isUnramifiedIn

∀ (K : Type u_1) (𝒪 : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsIntegralClosure 𝒪 ℤ K] {p : ℤ}, Prime p → (¬p ∣ NumberField.discr K ↔ Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p}))

A prime p does not divide discr K if and only if p (as the ideal span {p}) is unramified in the ring of integers 𝒪. Also see not_dvd_discr_iff_forall_liesOver and not_dvd_discr_iff_forall_mem for variants whose RHS does not use Algebra.IsUnramifiedIn.

Defined in

Mathlib.NumberTheory.NumberField.Discriminant.Different

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberFieldCommRingAlgebraIsIntegralClosure