Def SpectrumRestricts.starAlgHom

Modification history

2024-05-13 12:50

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean

refactor: generalize `SpectrumRestricts` to the `QuasispectrumRestricts`, preserving API (#12643)

Modified SpectrumRestricts.starAlgHom View on Github →

2024-03-07 08:49

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean

feat: restriction of the continuous functional calculus to a scalar subring (#10768)

Added SpectrumRestricts.starAlgHom View on Github →