Theorems · Theorem · number theory
NumberField.abs_discr_rpow_ge_of_isTotallyComplex
∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [NumberField.IsTotallyComplex K],
↑(Module.finrank ℚ K) ^ 2 / (4 / Real.pi * ↑(Module.finrank ℚ K).factorial ^ (2 * (↑(Module.finrank ℚ K))⁻¹)) ≤
↑|NumberField.discr K| ^ (↑(Module.finrank ℚ K))⁻¹- Cited by
- 0 results in Mathlib
- Foundations
- Depth 316 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites34
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · 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
- LT.lt.ne'proof · cited by 1,417
- le_of_ltproof · cited by 1,175
- NumberFieldstatement and proof · cited by 653
- Nat.factorialstatement and proof · cited by 616
- mul_posproof · cited by 374
- div_posproof · cited by 337
- pow_posproof · cited by 292
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.