Commit 2024-04-17 09:24 12c27420

feat: Define the covolume of a ZLattice (#11327) This PR defines the covolume of a Zlattice as the (finite) volume of any of its fundamental domain and proves some results about it, mainly: it's nonzero, it does not depend of the choice of the fundamental domain and it is equal to the absolute value of the determinant of any basis of the lattice. This PR also creates a directory Zlattice (with the original file becoming Zlattice/Basic.lean) and a new file Zlattice/Covolume.lean.