Commit 2024-06-01 21:26 13cef769

View on Github →

feat: instances of the non-unital continuous functional calculus for C⋆-algebras (#13365) This adds instances of the non-unital continuous functional calculus (for normal, selfadjoint and nonnegative elements) for non-unital C⋆-algebras.

Estimated changes

Modified Mathlib/Algebra/Algebra/Unitization.lean

added def Unitization.inrRangeEquiv

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

Modified Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean

added theorem CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts

added def CstarRing.spectralOrder

added theorem CstarRing.spectralOrderedRing

added theorem QuasispectrumRestricts.isSelfAdjoint

added theorem RCLike.nonUnitalContinuousFunctionalCalculus

added theorem cfcₙAux_id

added theorem cfcₙAux_mem_range_inr

added theorem closedEmbedding_cfcₙAux

added theorem isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts

added theorem nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts

added theorem spec_cfcₙAux

Modified Mathlib/Analysis/NormedSpace/Unitization.lean

added def Unitization.uniformEquivProd