measureReal_fundamentalDomain — Mathlib

English

The real-valued measure of the fundamental domain equals the real determinant of the matrix of the basis.

Русский

Десятичная мера фундаментальной области равна модулю детерминанта матрицы базиса.

LaTeX

$$$\mu_{\mathbb{R}}(\operatorname{fundamentalDomain}(b)) = |\det(\operatorname{Matrix.of} b)|.$$$

Lean4

theorem measureReal_fundamentalDomain [Fintype ι] [DecidableEq ι] [MeasurableSpace E] (μ : Measure E) [BorelSpace E]
    [Measure.IsAddHaarMeasure μ] (b₀ : Basis ι ℝ E) :
    μ.real (fundamentalDomain b) = |b₀.det b| * μ.real (fundamentalDomain b₀) := by
  simp [measureReal_def, measure_fundamentalDomain b μ b₀]

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