volume_fundamentalDomain_stdBasis

English

For x ∈ K, the mixedEmbedding norm equals the absolute value of the field norm of x.

Русский

Для x ∈ K норма смешанного вложения равна модулю нормa поля N_{ℚ}^{K}(x).

LaTeX

$$$ \|x\| = |\operatorname{Algebra.norm}_{\mathbb{Q}}(x)| $$$

Lean4

theorem volume_fundamentalDomain_stdBasis : volume (fundamentalDomain (stdBasis K)) = 1 :=
  by
  rw [fundamentalDomain_stdBasis, volume_eq_prod, prod_prod, volume_pi, volume_pi, pi_pi, pi_pi,
    Complex.volume_preserving_equiv_pi.measure_preimage ?_, volume_pi, pi_pi, Real.volume_Ico, sub_zero,
    ENNReal.ofReal_one, prod_const_one, prod_const_one, prod_const_one, one_mul]
  exact (MeasurableSet.pi Set.countable_univ (fun _ _ => measurableSet_Ico)).nullMeasurableSet

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