Commit 2024-10-27 18:23 d91cd427

View on Github →

feat: define the positive and negative parts of elements in a C⋆-algebra (#18103)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Quasispectrum.lean

modified theorem Unitization.quasispectrum_eq_spectrum_inr

Created Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/PosPart.lean

added theorem CFC.eq_negPart_iff

added theorem CFC.eq_posPart_iff

added theorem CFC.negPart_def

added theorem CFC.negPart_eq_zero_iff

added theorem CFC.negPart_mul_posPart

added theorem CFC.negPart_neg

added theorem CFC.negPart_nonneg

added theorem CFC.posPart_def

added theorem CFC.posPart_eq_zero_iff

added theorem CFC.posPart_mul_negPart

added theorem CFC.posPart_neg

added theorem CFC.posPart_nonneg

added theorem CFC.posPart_sub_negPart

Modified Mathlib/Analysis/Normed/Order/Lattice.lean