Hard Homogeneous Spaces

This file builds up the definition of a hard homogeneous space, an extension of a group action on some set such that the action of each group element defines a bijection. We use mathlib's AddTorsor type class to represent the bijection property, and extend this with finiteness and decidability conditions