English
The nonunital continuous functional calculus homomorphism cfcₙHom is defined from C(σₙ R a, R)₀ to A given p a.
Русский
Неединичный гомоморфизм непрерывного функционального калькулятора cfcₙHom задан для p a.
LaTeX
$$cfcₙHom : C(σₙ R a, R)₀ →⋆ₙₐ[R] A$$
Lean4
/-- The non-unital star algebra homomorphism underlying a instance of the continuous functional
calculus for non-unital algebras; a version for continuous functions on the quasispectrum.
In this case, the user must supply the fact that `a` satisfies the predicate `p`.
While `NonUnitalContinuousFunctionalCalculus` is stated in terms of these homomorphisms, in practice
the user should instead prefer `cfcₙ` over `cfcₙHom`.
-/
noncomputable def cfcₙHom : C(σₙ R a, R)₀ →⋆ₙₐ[R] A :=
(NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose
