Lattices (the other kind)

Stream: Is there code for X?

[Xavier Roblot]

I am looking for results about (real) lattices as used in the geometry of numbers, that is discrete subgroups of ℝ^n with applications to algebraic number theory in view. I see that Minkowski's theorem #2819 in closed to being added to mathlib so having lattices too could be very useful. For obvious reasons, doing a search for lattice in the docs is not very helpful :wink:

[Yaël Dillies]

docs#submodule is what you want. submodule int E is the type of lattices in the space E.

[Kevin Buzzard]

It's much bigger than the type of lattices in E, at least for the traditional number theorists use of the word "lattice" as a discrete cocompact subgroup.

[Xavier Roblot]

docs#submodule is what you want. submodule int E is the type of lattices in the space E.

Yes, I know that but what I am looking for are results about those. Mainly, things like the proof that a discrete subgroup of ℝ^n is a free ℤ-module of the same rank as the vector space it spans. I have some code to do that but I thought it might be there already.