Theorems · Theorem · number theory

NumberField.not_dvd_discr_iff_forall_liesOver

∀ (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 ↔
      ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P)

Also see not_dvd_discr_iff_forall_mem for a slightly easier to use RHS.

Defined in: Mathlib.NumberTheory.NumberField.Discriminant.Different
Cited by: 2 results in Mathlib
Foundations: Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field NumberField CommRing Algebra IsIntegralClosure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites39

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Setstatement · cited by 53,352
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
Idealstatement and proof · cited by 4,748
Algebra.algebraMapproof · cited by 4,706
IsDomainproof · cited by 2,196
LT.lt.ne'proof · cited by 1,417
Module.Finiteproof · cited by 1,032
Ideal.spanstatement and proof · cited by 948
CharZeroproof · cited by 932

Cited by2

Results whose statement or proof uses this declaration.

NumberField.not_dvd_discr_iff_isUnramifiedInproof · cited by 1
NumberField.not_dvd_discr_iff_forall_memproof · cited by 0