[Merged by Bors] - refactor: enforce the predicate on the ContinuousFunctionalCalculus is nontrivial

[j-loreaux]

add a condition to the unital and non-unital continuous functional calculus class which ensures that the predicate is nontrivial by requiring p 0 to hold. This guarantees in unital algebras that p (algebraMap R A r) holds, which is about all one can expect given that sometimes p := IsStarNormal.

---

see #14065 for motivation

[github-actions]

PR summary a3c62aa812

Import changes

No significant changes to the import graph

---

Declarations diff

+ cfc_predicate_algebraMap
+ cfc_predicate_one
+ cfc_predicate_zero
+ cfcₙ_predicate_zero
++-- cfc

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>

[j-loreaux]

@ADedecker I know you're busy with other things, but I would appreciate it if you could take a few minutes to review this. Frederic and I talked about it and think it makes sense, but I wanted to make sure you agree.

[dupuisf]

@ADedecker I understand you're a bit busy at the moment, so I'll just go ahead and merge this.

bors r+

[mathlib-bors]

Build failed:

• Build

[dupuisf]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style