dedekindZeta_residue_pos — Mathlib

English

The Dedekind zeta residue is strictly positive: 0 < dedekindZeta_residue(K).

Русский

Резидуал Dedekind zeta положителен: 0 < dedekindZeta_residue(K).

LaTeX

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

Lean4

theorem dedekindZeta_residue_pos : 0 < dedekindZeta_residue K :=
  by
  refine div_pos ?_ ?_
  · exact mul_pos (mul_pos (by positivity) (regulator_pos K)) (Nat.cast_pos.mpr (classNumber_pos K))
  ·
    exact
      mul_pos (Nat.cast_pos.mpr (torsionOrder_pos K)) <|
        Real.sqrt_pos_of_pos <| abs_pos.mpr (Int.cast_ne_zero.mpr (discr_ne_zero K))

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