feat: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot)

[MoritzBeroRoos]

Discussion at zulip.

Currently the abbreviations \cdot and \centerdot resolve to different, with the naked eye nearly undistinguishable symbols (despite the c in cdot surely standing for center..):

• \cdot gives ⬝ U+2B1D "Black Very Small Square"
• \centerdot gives · U+00B7 "Middle Dot"

Mathlib mostly uses the \centerdot variant, except for the dotProduct notation and some probably unsuspecting people wanting \centerdot but getting \cdot in their comments and 6 uses of a notation using the raw \cdot without any subscript at Mathlib\Topology\Homotopy\Product.lean.

This PR replaces the dot product ⬝ᵥ with its \centerdot counterpart ·ᵥ. The related PR here can then overwrite the \cdot abbreviation, to produce the same symbol as the centerdot abbreviation does.

---

[github-actions]

PR summary d3c295b45d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

Please put the PR description above the ---, otherwise it won't go in the commit message! There is no need to repeat the PR title.

[eric-wieser]

I think it might be a good idea to split this PR; so do a replavement of ·ᵥ back with ⬝ᵥ, since it seems all the other dots are just mistakes! Then we can replace just dotProduct in a follow-up PR.

[MoritzBeroRoos]

i have rolled back all changes, and in this pr replace only the dotproduct notation.
(i saw your message after i had already edited everything here, sorry).
How can i build a pr on top of this one? The other one would change all the comments, leaving only the homotopy product with the \cdot variant

[eric-wieser]

I claim we should actually use

Suggested change

	* `·ᵥ` for `dotProduct`
	* `⋅ᵥ` for `dotProduct`

but let's wait for a zulip opinion