[Merged by Bors] - feat(algebra/module/zlattice): prove some results about Z-lattices

[xroblot]

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

---

• depends on: [Merged by Bors] - feat(analysis/normed/order/lattice): add has_solid_norm #18554
• depends on: [Merged by Bors] - feat(linear_algebra/basis): add basis.restrict_scalars #18814
• depends on: [Merged by Bors] - feat(algebra/module/submodule/basic): add has_vadd #18815

[alexjbest]

I wonder how general we should make this file, clearly some of the bits at the end are quite specific to Z inside R, but results like zspan.mem_span_iff seem useful more generally for quite arbitrary spans of subrings?

[riccardobrasca]

Thanks!

bors d+

[bors]

✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[xroblot]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests