English
For a fractional ideal I, the covolume of the associated mixedEmbedding.idealLattice equals absNorm(I) times the same discriminant factor as above.
Русский
Для дробного идеала I коволюм связанной с ним смеси решетки равен absNorm(I) умножить на дискриминанс-фактор.
LaTeX
$$$\mathrm{ZLattice.covolume}(\mathrm{mixedEmbedding.idealLattice}(K, I)) = \mathrm{absNorm}(I) \cdot 2^{-nrComplexPlaces(K)} \cdot \sqrt{|\mathrm{discr}(K)|}$$$
Lean4
theorem _root_.NumberField.mixedEmbedding.covolume_idealLattice (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
ZLattice.covolume (mixedEmbedding.idealLattice K I) =
(FractionalIdeal.absNorm (I : FractionalIdeal (𝓞 K)⁰ K)) * (2⁻¹) ^ nrComplexPlaces K * √|discr K| :=
by
rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_idealLattice K I), measureReal_def,
volume_fundamentalDomain_fractionalIdealLatticeBasis, volume_fundamentalDomain_latticeBasis, ENNReal.toReal_mul,
ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_inv, toReal_ofNat, ENNReal.coe_toReal, Real.coe_sqrt,
coe_nnnorm, Int.norm_eq_abs, ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.val)),
mul_assoc]
