feat(geometry/euclidean/lattice): define standard square lattice in the affine plane

[hrmacbeth]

Given a Euclidean affine plane P modelled on ℂ, I define the type square_lattice P of lattices in P modelled on the integer lattice in ℂ, being careful to do this in such a way that square_lattice P has no distinguished basepoint.

---

Marked as WIP while I think about a couple of things; maybe one needs also square lattices of arbitrary side length, and also the "diamond" lattice of every second point in a square lattice.

• [x] depends on: #8814

[github-actions[bot]]

This PR/issue depends on:

• ~~leanprover-community/mathlib#8814~~ By Dependent Issues (🤖). Happy coding!

[YaelDillies]

I suspect #18266 does things better by allowing an arbitrary basis.