covolume_integerLattice — Mathlib

English

The covolume of the mixed embedding lattice is given by the discriminant and complex places via a product formula.

Русский

Ковольюм решетки смешанного вложения выражается через дискриминант и комплексные места в виде произведения.

LaTeX

$$$\mathrm{covolume}(\text{mixedEmbedding.idealLattice}(K)) = \mathrm{absNorm}(I) \cdot 2^{-(nrComplexPlaces(K))} \cdot \sqrt{|\mathrm{discr}(K)|}$$$

Lean4

theorem _root_.NumberField.mixedEmbedding.covolume_integerLattice :
    ZLattice.covolume (mixedEmbedding.integerLattice K) = (2⁻¹) ^ nrComplexPlaces K * √|discr K| := by
  rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_integerLattice K), measureReal_def,
    volume_fundamentalDomain_latticeBasis, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_inv, toReal_ofNat,
    ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm, Int.norm_eq_abs]

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