[WIP] Remove pre-Lorentz vectors Co, Contr, etc.

[Copilot]

Thanks for asking me to work on this. I will get started on it and keep this PR's description up to date as I form a plan and make progress.

---

This section details on the original issue you should resolve

<issue_title>Removing pre-Lorentz vectors Co, Contr etc.</issue_title>
<issue_description>The current implementation of Lorentz vectors in Lean, defines some preliminary modules and representations, these include Co, Contr etc.

These can be removed and simply replaced with Vector and CoVector, with a careful seperation of definitions into the required modules. Similar for the complex case.</issue_description>

Comments on the Issue (you are @copilot in this section)