[Merged by Bors] - chore: removes non-breaking spaces (U+00a0)

[adomasbaliuka]

Removes all non-breaking spaces (U+00a0) from Mathlib.

This is in preparation for using the "unicode linter" (#16215), which would (as of now) disallow non-printing characters except for space (U+0020) and linefeed (U+000A).

---

Relevant discussions:

• Zulip

• feat(Tactic/Linter): lint unwanted unicode #16215

[github-actions]

PR summary 029839cae9

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.

[grunweg]

Are there any such spaces in the archive, tests or counterexamples?
(This need not block this PR; I think these changes are useful in any case.)

[grunweg]

Thanks!
maintainer merge

[github-actions]

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

[adomasbaliuka]

Are there any such spaces in the archive, tests or counterexamples? (This need not block this PR; I think these changes are useful in any case.)

As far as I can see, there are no more in the entire repository.

[sgouezel]

bors r+
Thanks!

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[adomasbaliuka]

@sgouezel it seems that a linter complains about a too long line in a file this PR didn't change? How can that happen? Probably has something to do with the fact that the line-length linter was changed earlier today?

[mathlib-bors]

Build failed (retrying...):

• Lint style

[mathlib-bors]

Build failed:

• Lint style

[sgouezel]

bors r+

[mathlib-bors]

Build failed (retrying...):

• Build

[adomasbaliuka]

@grunweg @sgouezel the "overlong" line that the bors build complains about isn't actually overlong. So I have no idea what's happening here...

[bryangingechen]

The lint failure might be from another PR currently being merged or from a commit in master which isn't in this branch yet. In any case this PR now has a merge conflict with master as well, so I'm taking it off the queue:
bors r-

After merging master and fixing any errors, feel free to put this back on the queue:
bors d+

[mathlib-bors]

✌️ adomasbaliuka can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mathlib-bors]

Canceled.

[adomasbaliuka]

bors r+

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style