[Merged by Bors] - feat: add the cdot linter

[adomani]

The cdot linter is a syntax linter that flags uses of the "cdot" · that are achieved by typing a character different from ·.

For instance, a "plain" dot . is allowed syntax, but is flagged by the linter.

---

[github-actions]

PR summary 7c2a5b94f1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ cdotLinter
+ findCDot
+ getLinterHash
+ instance : Inhabited Nat
+ isCDot?
+ unwanted_cdot

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>

[grunweg]

Looks great in general! Here's a first round of small comments: I'll eat now, and will return to this afterwards.

[grunweg]

Thanks for writing this! I just pushed a commit with tiny style-only tweaks directly.
Looks good to me now.
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[dupuisf]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style