feat: the translation operator

[YaelDillies]

Define translation of a function by an element of its domain

From LeanAPAP

---

I don't really like this code, but it is foundational for discrete analysis and I have found no nice way around using it. I would like to know @urkud's opinion as I am aware he needs translation for dynamical systems. Here are a few points of concern I am aware of:

• There is no multiplicative version. That's because I do not need the multiplicative version and wouldn't know how to call it
• This is basically an action by DomMulAct. The trouble is that it would be inconvenient to state it this way because I would also need to stick some op in there. And generally this action is wide-spread in LeanAPAP and I want custom notation for it.