[Merged by Bors] - feat(ContinuousFunctionalCalculus): add several lemmas involving the CFC and algebraMap

[dupuisf]

This PR adds several lemmas about the interaction between the (non-unital) CFC and algebraMap. Several lemmas require some sort of nontriviality statement for the CFC (i.e. the predicate can't be false everywhere), I just stated it as an hp : p 0 hypothesis in the lemma statements; it seems like the most convenient way in practice and probably the easiest to automate.

Co-authored-by: Jireh Loreaux [email protected]

---

• depends on: [Merged by Bors] - refactor: enforce the predicate on the ContinuousFunctionalCalculus is nontrivial #14100

[github-actions]

PR summary fdb45dba34

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ CFC.eq_algebraMap_of_spectrum_subset_singleton
+ CFC.eq_one_of_spectrum_subset_one
+ CFC.eq_zero_of_quasispectrum_eq_zero
+ CFC.eq_zero_of_spectrum_subset_zero
+ CFC.quasispectrum_zero_eq
+ CFC.spectrum_algebraMap_eq
+ CFC.spectrum_algebraMap_subset
+ CFC.spectrum_one_eq
+ CFC.spectrum_zero_eq
+ cfc_algebraMap
+ cfc_apply_one
+ cfc_apply_zero
+ cfcₙ_apply_zero
- eq_algebraMap_of_spectrum_subset_singleton
- eq_one_of_spectrum_subset_one
- eq_zero_of_quasispectrum_eq_zero
- eq_zero_of_spectrum_subset_zero

You can run this locally as follows

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

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

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor: enforce the predicate on the ContinuousFunctionalCalculus is nontrivial #14100
  By Dependent Issues (🤖). Happy coding!

[j-loreaux]

bors d+

[mathlib-bors]

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

[dupuisf]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style