Commit 2024-07-08 16:00 31d24779

chore: Added namespace Mathlib around Vector defs (#13407) This PR puts Mathlib.Data.Vector's Vector type into the namespace Mathlib. This will help ensure that users of Mathlib and Batteries can use this Vector type and Batteries' upcoming Array based Vector type without name conflicts. Tasks:

• Put all Vector definitions, currently all of which are inside Mathlib/Data/Vector into the namespace Mathlib. - [x] Add deprecation aliases for all defs, theorems and lemmas thus namespaced. NOTE : This is not possible because alias simply reintroduces naming conflicts. See the linked zulip discussion
• Fix breakages within Mathlib Discussion in Zulip topic