Commit 2025-11-04 20:27 7f1e069f

View on Github →

chore(Analysis/CStarAlgebra/CFC/Order): relate section to strict positivity (#30694)

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

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

modified theorem CFC.conjugate_rpow_neg_one_half

modified theorem CStarAlgebra.isUnit_of_le

modified theorem CStarAlgebra.rpow_neg_one_le_rpow_neg_one

modified theorem le_iff_norm_sqrt_mul_rpow