Mathlib

An action is a homomorphism G → Sym(X). The group moves the points.