Theorem CStarAlgebra.nonneg_iff_eq_isSelfAdjoint_mul_self

Modification history

2025-09-27 15:46

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

chore(Analysis/SpecialFunctions/CFC/Rpow/Basic): fix confusing names (#30031) …

Deleted CStarAlgebra.nonneg_iff_eq_isSelfAdjoint_mul_self View on Github →

2025-09-16 11:11

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

feat(Analysis/SpecialFunctions/CFC/Rpow): `0 ≤ a` iff `a = star b * b` for some `b` (#29592) …

Added CStarAlgebra.nonneg_iff_eq_isSelfAdjoint_mul_self View on Github →