Commit 2026-06-23 15:06 a163fd2f

View on Github →

feat: introduce SelfAdjointDecompose class (#40530)

Estimated changes

Modified Mathlib/Algebra/Order/Star/Basic.lean

added theorem IsSelfAdjoint.exists_nonneg_sub_nonneg

added theorem IsSelfAdjoint.map'

Modified Mathlib/Algebra/Order/Star/Real.lean

Modified Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean

deleted theorem map_isSelfAdjoint

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Basic.lean

Modified Mathlib/LinearAlgebra/Complex/Module.lean

added theorem map_imaginaryPart

added theorem map_realPart