Mathlib Changelog
v4
Changelog
About
Github
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