exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr

English

For a fractional ideal I of the ring of integers, the covolume of the mixedEmbedding.idealLattice equals absNorm(I) times the usual discriminant factor.

Русский

Для дробного идеала 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 exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr :
    ∃ (a : 𝓞 K),
      a ≠ 0 ∧
        |Algebra.norm ℚ (a : K)| ≤
          (4 / π) ^ nrComplexPlaces K * (finrank ℚ K).factorial / (finrank ℚ K) ^ (finrank ℚ K) * Real.sqrt |discr K| :=
  by
  obtain ⟨_, h_mem, h_nz, h_nm⟩ := exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K ↑1
  obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
  refine ⟨a, ne_zero_of_map h_nz, ?_⟩
  simp_rw [Units.val_one, FractionalIdeal.absNorm_one, Rat.cast_one, one_mul] at h_nm
  exact h_nm

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