abs_discr_rpow_ge_of_isTotallyComplex

English

0 < dedekindZeta_residue(K).

Русский

0 < dedekindZeta_residue(K).

LaTeX

$$$0 < \mathrm{dedekindZeta\_residue}(K)$$$

Lean4

theorem abs_discr_rpow_ge_of_isTotallyComplex [IsTotallyComplex K] :
    (finrank ℚ K) ^ 2 / ((4 / π) * (finrank ℚ K).factorial ^ (2 * (finrank ℚ K : ℝ)⁻¹)) ≤
      |discr K| ^ (finrank ℚ K : ℝ)⁻¹ :=
  by
  have h : 0 < (finrank ℚ K : ℝ) := Nat.cast_pos.mpr finrank_pos
  rw [← Real.rpow_le_rpow_iff (z := finrank ℚ K) (by positivity) (by positivity) h,
    Real.div_rpow (by positivity) (by positivity), ← Real.rpow_mul (by positivity), inv_mul_cancel₀ h.ne',
    Real.rpow_one, Real.mul_rpow (by positivity) (by positivity), Real.rpow_natCast, Real.rpow_natCast, ← pow_mul, ←
    Real.rpow_mul (by positivity), inv_mul_cancel_right₀ h.ne', Real.rpow_two]
  exact abs_discr_ge_of_isTotallyComplex K

Похожие утверждения