volume_real_fundamentalDomain — Mathlib

English

The real-valued volume of the fundamental domain is the absolute value of the determinant of the matrix of the basis.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem volume_real_fundamentalDomain [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ (ι → ℝ)) :
    volume.real (fundamentalDomain b) = |(Matrix.of b).det| := by simp [measureReal_def]

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