Say I'm formalizing something in group theory, and I'm working with some action $\cdot$ of $(G, +)$ on a set. In my math textbook, the identity of $\cdot$ is explicitly mentioned once (if that), and then left implicit. In my formalization, do I have to constantly keep specifying $(G, \cdot)$, or can I temporarily set $\cdot$ as the default?
In my limited experience, mathematical writing uses "dynamic scope" like this a lot. Does this actually correspond to a computer scientist's definition of dynamic scope, and if so, do any proof assistants support this?