Commit 2024-10-29 22:19 2fcccf33

View on Github →

feat: (cfcₙ f a : A⁺¹) = cfc f (a : A⁺¹) (#18358)

Estimated changes

Modified Mathlib/Algebra/Algebra/Quasispectrum.lean

added theorem Unitization.quasispectrum_inr_eq

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

added theorem Unitization.cfcₙ_eq_cfc_inr

added theorem Unitization.complex_cfcₙ_eq_cfc_inr

added theorem Unitization.real_cfcₙ_eq_cfc_inr

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

modified theorem Unitization.inr_nonneg_iff

added theorem Unitization.nnreal_cfcₙ_eq_cfc_inr