Theorems · Theorem · number theory

NumberField.abs_discr_ge_of_isTotallyComplex

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [NumberField.IsTotallyComplex K],
  ↑(Module.finrank ℚ K) ^ (2 * Module.finrank ℚ K) /
      ((4 / Real.pi) ^ Module.finrank ℚ K * ↑(Module.finrank ℚ K).factorial ^ 2) ≤
    ↑|NumberField.discr K|

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

Realstatement · cited by 25,697
Fieldstatement and proof · cited by 7,404
absstatement and proof · cited by 1,814
Real.pistatement and proof · cited by 1,774
Module.finrankstatement and proof · cited by 1,770
NumberFieldstatement and proof · cited by 653
Nat.factorialstatement and proof · cited by 616
NumberField.discrstatement and proof · cited by 53
NumberField.InfinitePlace.nrComplexPlacesproof · cited by 52
NumberField.IsTotallyComplexstatement and proof · cited by 19
NumberField.abs_discr_ge'proof · cited by 2
NumberField.IsTotallyComplex.finrankproof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

NumberField.abs_discr_rpow_ge_of_isTotallyComplexproof · cited by 0