Theorems · Theorem · number theory

RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  ↑|NumberField.discr K| <
      (2 * (Real.pi / 4) ^ NumberField.InfinitePlace.nrComplexPlaces K *
          (↑(Module.finrank ℚ K) ^ Module.finrank ℚ K / ↑(Module.finrank ℚ K).factorial)) ^
        2 →
    IsPrincipalIdealRing (NumberField.RingOfIntegers K)

Defined in: Mathlib.NumberTheory.NumberField.ClassNumber
Cited by: 2 results in Mathlib
Foundations: Depth 315 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field NumberField

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites40

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

DFunLike.coeproof · cited by 62,936
Realstatement and proof · cited by 25,697
Fieldstatement and proof · cited by 7,404
Idealproof · cited by 4,748
le_antisymmproof · cited by 2,068
absstatement and proof · cited by 1,814
Real.pistatement and proof · cited by 1,774
Module.finrankstatement and proof · cited by 1,770
mul_assocproof · cited by 1,667
le_of_ltproof · cited by 1,175
nonZeroDivisorsproof · cited by 895
NumberFieldstatement and proof · cited by 653

Cited by2

Results whose statement or proof uses this declaration.

IsCyclotomicExtension.Rat.five_pidproof · cited by 0
IsCyclotomicExtension.Rat.three_pidproof · cited by 0