Commit 2023-08-20 13:35 0db562a3

feat(Algebra.Module.Zlattice): add Zlattice.module_free and Zlattice.rank (#5728) We prove the main characterisation of $\mathbb{Z}$-lattices: a subgroup $L$ of $\mathbb{R}^n$ that is discrete and that spans $\mathbb{R}^n$ is a free $\mathbb{Z}$-module of rank $n$ (in a slightly more general setting).