2024-05-29 20:55
Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean
feat: restriction of the non-unital continuous functional calculus to a scalar subring (#13327) …
Added QuasispectrumRestricts.closedEmbedding_nonUnitalStarAlgHom