Commit 2024-04-05 21:50 01622329

feat: Add Zspan.fundamentalDomain_ae_parallelepiped (#11321) Prove that the fundamental domain of a ℤ-lattice is almost equal to the corresponding parallelepiped. This is useful because many results in measure theory use the parallelepiped associated to a basis.