volume_fundamentalDomain — Mathlib

English

The volume of the fundamental domain equals the determinant of the basis in the ambient real space.

Русский

Объём фундаментальной области равен определителю базиса в окружающем вещественном пространстве.

LaTeX

$$$\text{volume}(\operatorname{fundamentalDomain}(b)) = |\det(\operatorname{Matrix.of} b)|.$$$

Lean4

@[simp]
theorem volume_fundamentalDomain [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ (ι → ℝ)) :
    volume (fundamentalDomain b) = ENNReal.ofReal |(Matrix.of b).det| :=
  by
  rw [measure_fundamentalDomain b volume (b₀ := Pi.basisFun ℝ ι), fundamentalDomain_pi_basisFun, volume_pi,
    Measure.pi_pi, Real.volume_Ico, sub_zero, ENNReal.ofReal_one, Finset.prod_const_one, mul_one, ←
    Matrix.det_transpose]
  rfl

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