mathlib3

a3e83f0f - feat(algebra/module/zlattice): prove some results about Z-lattices (#18266)

feat(algebra/module/zlattice): prove some results about Z-lattices (#18266) For a ℤ-lattice `L` given by `L := submodule.span ℤ (set.range b)` where `b` is a basis of finite dimensional real vector space `E`, this PR defines the fundamental domain of `L` and proves that it is a fundamental domain in the sense of `measure_theory.group.fundamental_domain`. It also introduces most of the tools that will be needed to prove that a discrete subgroup of `E` that spans `E` over `ℝ` is a ℤ-lattice, see #18477