Commit 2023-09-14 13:42 11bd532d

feat: add results for the computation of the volume of Zspan.fundamentalDomain (#6904) We prove that the covolume of a $\mathbb{Z}$-lattice of $\mathbb{R}^n$ generated by the basis $b$ is equal to the absolute value of the determinant of the matrix formed by the vectors of $b$, that is

theorem volume_fundamentalDomain [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ (ι → ℝ)) :
     volume (fundamentalDomain b) = ENNReal.ofReal |(Matrix.of b).det|