Ends of groups: a nonstandard perspective #
Inspired by the paper we give a definition of the Cayley graph of a group. We start from Kyle Miller's Lean 3 code at https://leanprover-community.github.io/archive/stream/217875-Is-there-code-for-X%3F/topic/graph.2C.20expander.20graph.2C.20cayley.20graph.2C.20.2E.2E.2E.html
After converting that to Lean 4, we construct the Cayley graph of ℤ and give some computations on it.
We also construct a path in this Cayley graph, using Lean's Quiver.Path.