Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-03-07 08:49
d7714b7c
View on Github →
feat: restriction of the continuous functional calculus to a scalar subring (
#10768
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean
added
theorem
SpectrumRestricts.compactSpace
added
def
SpectrumRestricts.starAlgHom