feat: the positive and negative parts of a selfadjoint element in a C⋆-algebra are unique

[j-loreaux]

---

• [ ] depends on: #18103
• [ ] depends on: #18116
• [ ] depends on: #18117
• [ ] depends on: #18118
• [ ] depends on: #18126
• [ ] depends on: #18128

[github-actions[bot]]

PR summary 672955f4c3

Import changes exceeding 2%

%	File
+13.52%	Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.PosPart

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.PosPart	1516	1721	+205 (+13.52%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.PosPart	205

---

Declarations diff

+ posPart_negPart_unique

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#18103~~
• ~~leanprover-community/mathlib4#18116~~
• ~~leanprover-community/mathlib4#18117~~
• ~~leanprover-community/mathlib4#18118~~
• ~~leanprover-community/mathlib4#18126~~
• ~~leanprover-community/mathlib4#18128~~ By Dependent Issues (🤖). Happy coding!

[mathlib-bors[bot]]

:v: j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[j-loreaux]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style