Commit 2024-10-24 15:52 e1f8635a

View on Github →

refactor: create CStarAlgebra classes and refactor to use them (#16953)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/CStarAlgebra/Classes.lean

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

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

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

Created Mathlib/Analysis/CStarAlgebra/ContinuousLinearMap.lean

Created Mathlib/Analysis/CStarAlgebra/ContinuousMap.lean

Modified Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

modified theorem gelfandStarTransform_naturality

Modified Mathlib/Analysis/CStarAlgebra/Hom.lean

modified theorem IsSelfAdjoint.map_spectrum_real

Modified Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean

Modified Mathlib/Analysis/CStarAlgebra/Module/Defs.lean

modified theorem CStarModule.inner_mul_inner_swap_le

modified theorem CStarModule.norm_eq_csSup

modified theorem CStarModule.norm_inner_le

modified theorem CStarModule.normedSpaceCore

Modified Mathlib/Analysis/CStarAlgebra/Multiplier.lean

Modified Mathlib/Analysis/CStarAlgebra/Spectrum.lean

Modified Mathlib/Analysis/CStarAlgebra/Unitization.lean

Created Mathlib/Analysis/CStarAlgebra/lpSpace.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/StarOrder.lean

Modified Mathlib/Analysis/Normed/Lp/lpSpace.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean

Modified Mathlib/Analysis/VonNeumannAlgebra/Basic.lean

Modified Mathlib/Topology/ContinuousMap/Compact.lean