English
The covolume of the integer lattice under the mixed embedding equals 2^{−nrComplexPlaces(K)} times sqrt(|discr(K)|).
Русский
Ковольюм целочисленной решетки в смешанном вложении равен 2^{−nrComplexPlaces(K)} умножить на sqrt(|discr(K)|).
LaTeX
$$$\mathrm{covolume}(\text{mixedEmbedding.integerLattice}(K)) = 2^{-nrComplexPlaces(K)} \cdot \sqrt{|\mathrm{discr}(K)|}$$$
Lean4
theorem isPrincipalIdealRing_of_abs_discr_lt
(h : |discr K| < (2 * (π / 4) ^ nrComplexPlaces K * ((finrank ℚ K) ^ (finrank ℚ K) / (finrank ℚ K)!)) ^ 2) :
IsPrincipalIdealRing (𝓞 K) := by
have : 0 < finrank ℚ K := finrank_pos
rw [← Real.sqrt_lt (by positivity) (by positivity), mul_assoc, ← inv_mul_lt_iff₀' (by positivity), mul_inv, ← inv_pow,
inv_div, inv_div, mul_assoc, Int.cast_abs] at h
refine isPrincipalIdealRing_of_isPrincipal_of_norm_le (fun I hI ↦ ?_)
rw [absNorm_eq_one_iff.mp <|
le_antisymm (lt_succ.mp (cast_lt.mp (lt_of_le_of_lt hI h))) <|
one_le_iff_ne_zero.mpr (absNorm_ne_zero_of_nonZeroDivisors I)]
exact top_isPrincipal
