Commit 2026-08-15 19:39 816148f1

View on Github →

refactor(Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order): clean up hypotheses (#42545)

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

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

modified theorem CStarAlgebra.mul_star_le_algebraMap_norm_sq

added theorem CStarAlgebra.nnnorm_le_nnnorm_of_le_of_nonneg

deleted theorem CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le

modified theorem CStarAlgebra.nnnorm_mem_spectrum_of_nonneg

added theorem CStarAlgebra.norm_le_norm_of_le_of_nonneg

deleted theorem CStarAlgebra.norm_le_norm_of_nonneg_of_le

modified theorem CStarAlgebra.norm_mem_spectrum_of_nonneg

modified theorem CStarAlgebra.norm_or_neg_norm_mem_spectrum

modified theorem CStarAlgebra.pow_antitone

modified theorem CStarAlgebra.pow_nonneg

modified theorem CStarAlgebra.star_left_conjugate_le_norm_smul

modified theorem CStarAlgebra.star_mul_le_algebraMap_norm_sq

modified theorem CStarAlgebra.star_right_conjugate_le_norm_smul

modified theorem IsSelfAdjoint.le_algebraMap_norm_self

modified theorem IsSelfAdjoint.neg_algebraMap_norm_le_self

modified theorem IsSelfAdjoint.toReal_spectralRadius_eq_norm

deleted theorem Unitization.inr_le_iff

added theorem Unitization.inr_le_inr_iff

added theorem Unitization.inr_nonneg

added theorem Unitization.nonneg_of_inr

modified theorem Unitization.sqrt_inr

modified theorem le_iff_norm_sqrt_mul_sqrt_inv

Modified Mathlib/Analysis/CStarAlgebra/GelfandNaimarkSegal.lean

Modified Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean

Modified Mathlib/Analysis/CStarAlgebra/Module/Defs.lean

Modified Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean

Modified Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean